Job 2165

CakeML:56a83d59d928f8670f6a12210c89b29fdc084d27
  More permissive no_closures and minor tidy up [Jul 13 21:09:55]
#962 (fix-no-clos)
Merging into:c530285ee87d71e48f9f1f5689976e9dca729e35
  Merge pull request #960 from CakeML/pan_parse_build [Jul 13 08:44:54]
HOL:b0b4d6822b4ca1fb28417db0427d08d61e121d17
  Fix Unicode; other minor tidy-ups [Jul 05 06:01:40]
Machine:oven0 5.19.0-46-generic x86_64 GNU/Linux

Jul 13 21:18:16 Claimed job
Jul 13 21:18:21 Building HOL