Job 2939

CakeML:bf32a6ef593496f17fcebaf2b2dac18fb6b10cae
  More git-ignore fixes [Aug 22 02:38:55]
#1210 (revisedFloats)
Merging into:b68e46f49bc81902b1785c5861e13b9385818aa4
  Merge pull request #1218 from CakeML/build-tweaks [Aug 22 08:10:51]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 22 09:06:49 Claimed job
Aug 22 09:06:53 Reusing HOL
Aug 22 09:07:01 Starting developers
Aug 22 09:07:05 Finished developers                                               3s 197MB
Aug 22 09:07:06 Starting developers/bin
Aug 22 09:07:11 Finished developers/bin                                           4s 594MB
Aug 22 09:07:12 Starting misc
Aug 22 09:07:52 Finished misc                                                    39s   1GB
Aug 22 09:07:53 Starting compiler/proofs Aug 22 09:07:53 5080s