History for marking / .gitignore
2023-06-06
Add more complete .gitignore
Mark George committed on 6 Jun
Add jdtls stuff to ignorefile
Mark George committed on 6 Jun
2022-06-17
Change 'special' criterion to text fields. ...
Mark George committed on 17 Jun 2022
Minor cleanup. Library updates. Update schema to latest version.
Mark George committed on 17 Jun 2022
2016-09-04
Special criterion added. Marking properties added. Remember last selection.
Mark committed on 4 Sep 2016