Job 2671

CakeML:b562031a45762ae7bdef8c1a2f02c4660d33b65e
  Fix typo in parse error handling code [Oct 18 08:35:54]
#1073 (pan_parseErrFix)
Merging into:b94ca1db7fb392d05ab143a451a30f7a5ba3390d
  Adjust @myreen's editor settings [Oct 18 21:56:34]
HOL:07c84bff2b89ddb2c81c57884f4141bbc37accdb
  Fix cv_compute regression test to cope with case-sensitive files [Oct 15 03:20:04]
Machine:pavlova

Oct 18 22:12:51 Claimed job
Oct 18 22:12:54 Reusing HOL