Extend Instrument repository to remove files

[Nick Draper]

Only ever from the appdataq dir and only when the files are not present on github.

[Nick Draper]

re #10661 If file removed from github, remove from appdata instrument

Changeset: d6dae254918b329257d96271bf3262101990442f

[Nick Draper]

re #10661 remove linux warning

Changeset: d8429274746c13cc7f627caace8e66c3f22cbc05

[Nick Draper]

To Test

We don't want to go altering the instrument repository on master, so we will test it by adding an orphaned file instead.

1. Startup mantidplot
2. find your appdata instrument directory by running this

   print ConfigService.getInstrumentDirectories()[0];
   

3. Go to that directory and
   1. Delete github.json if present
   2. Add an empty file "orphaned.xml"
4. Run the DownloadInstrument alg with the log in debug.
5. The orphaned.xml should be deleted, with some debug level messages about it.

The bigger question -Resolved see comment 6

Should we do this? The .mantid/instrument directory gives linux users a writable location they can drop edited instrument files and have them used by mantid. This change would delete any local only files on each startup.

[Nick Draper]

re #10661 remove linux warning

Changeset: c8ccb57a436749c72e233bc4ce39bd3ea64dc3fe

[Nick Draper]

The bigger question has been resolved in a conversation with Pete Peterson. This directory is not currently used by anyone, and no user knows about it. At the SNS users don't fiddle with instrument files. So this is not an issue.

Free to be tested by anyone.

[Harry Jeffery]

Merge remote-tracking branch 'origin/feature/10661_support_inst_repo_file_removal'

Full changeset: ​118281bc22b0010f59aca5cc9cc114675e87b66a

[Stuart Campbell]

This ticket has been transferred to github issue ​11503