Job 2896

CakeML:b9b9b265413ab0452bcc29ddfebe33a5a00cb187
  More set_grammar_ancestry [Jul 18 08:35:55]
#1202 (set_grammar_ancestry)
Merging into:438ba42d07076a8f14c147c24a56b265ce72accd
  Merge pull request #1199 from CakeML/wordLang_multiret [Jul 29 06:29:57]
HOL:a81865b9bac5e3018a070980ce8f4a392c66c9c6
  Get Holmake and build to clean properly given .hol directory [Jul 07 07:18:21]
Machine:lammmington

Aug 01 00:44:16 Claimed job
Aug 01 00:44:22 Reusing HOL
Aug 01 00:44:30 Starting developers
Aug 01 00:44:34 Finished developers                                               3s 214MB
Aug 01 00:44:35 Starting developers/bin
Aug 01 00:44:40 Finished developers/bin                                           3s 592MB
Aug 01 00:44:41 Starting misc
Aug 01 00:45:23 Finished misc                                                    40s   2GB
Aug 01 00:45:23 Starting compiler/proofs Aug 01 00:45:23 5873s