Job 2927

CakeML:e73a00ac4a308584c589c8abc954da8e6368bb84
  Remove now-deleted flover directories from build-sequence [Aug 20 07:32:15]
#1210 (revisedFloats)
Merging into:786090f5e6275158b2b6020250c42733e42ed6dd
  Merge pull request #1217 from CakeML/pancake_globals [Aug 20 10:55:37]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:lammmington

Aug 20 11:09:55 Claimed job
Aug 20 11:09:58 Reusing HOL
Aug 20 11:10:06 Starting developers
Aug 20 11:10:07 FAILED: developers
Starting work on lint_build_dirs
lint_build_dirs                                                     (0s)     OK
Starting work on lint
lint                                                                (0s)FAIL<1>
 The following paths in build-sequence do not contain a Holmakefile:
 icing/
 Full log: /scratch/cakeml/regression3/cakeml-2927/developers/.hol/logs/lint
readme_gen                                                          (0s)MKILLED