Job 2430

CakeML:e03a6548d91c8d2189ec62ce0dc4e9fdfa85083b
  Merge pull request #1 from IlmariReissumies/pancake_entry_points [Jun 29 01:38:41]
#1005 (pancake_entry_points)
Merging into:a14567ec355683fa0b4865d412e74610e3e1f1ae
  Merge pull request #1004 from DoomishGuy/pan_lower_ops [Jun 26 10:21:07]
HOL:493fc3fcd7d8390b7d85861775b6e56fd6b17d9f
  Remove some unicode [Jun 18 04:19:36]
Machine:lammmington

Jun 29 01:42:05 Claimed job
Jun 29 01:42:14 Building HOL
Jun 29 01:56:28 Starting developers
Jun 29 01:56:32 Finished developers                                               2s 214MB
Jun 29 01:56:33 Starting developers/bin
Jun 29 01:56:44 Finished developers/bin                                          10s   1GB
Jun 29 01:56:45 Starting compiler/proofs Jun 29 01:56:45 6528s