Job 2137

CakeML:73d4774786232785747eb170136ad5ade9ed882c
  Remove trailing whitespace. [May 18 01:34:30]
#954 (pan_parser_funs)
Merging into:5e0612a6f93d34e570019c2a768cbd4736402abe
  Fix for change to finite_mapSyntax in HOL [May 25 02:29:21]
HOL:b714d6b6c7a82ffd8f7fc64afb34d214f058a0bf
  Update building and testing of Manual/Tools/polyscripter [May 24 05:50:35]
Machine:pavlova

May 26 07:37:12 Claimed job
May 26 07:37:16 Building HOL
May 26 07:38:59 FAILED: building HOL