Job 2990

CakeML:dca57e2e072549f2e98f1a19a68e18d6c133bb8f
  Merge remote-tracking branch 'refs/remotes/origin/thunks' into thunks [Oct 01 01:46:52]
#1246 (thunks)
Merging into:6ddaf6f8d86d8d5f57f0bcfc8fdd78f855e3daae
  Make it clearer that HOL master should be used [Sep 29 10:18:48]
HOL:77749ad4d0926abb872e3704d8b98abc98f87c73
  Decompiler into Interaction Trees (#1664) [Sep 29 12:05:48]
Machine:pavlova

Oct 01 05:28:24 Claimed job
Oct 01 05:28:28 Reusing HOL
Oct 01 05:28:35 Starting developers
Oct 01 05:28:40 Finished developers                                               3s 164MB
Oct 01 05:28:41 Starting developers/bin
Oct 01 05:28:45 Finished developers/bin                                           2s  89MB
Oct 01 05:28:45 Starting misc
Oct 01 05:28:46 FAILED: misc
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Holmake: Attempt to recurse into non-existent directory: $(HOLDIR)/examples/fun-op-sem/lprefix_lub
  (Probably a result of bad INCLUDES spec.)