Overview

Job 3407

CakeML:55293f8d4e276d23ebe13f0619e261af16b914a3
  Factor the per-directory README.md rule into developers/readme.mk.
#1422 (common-readme-target)
Merging into:e0e4e28e48d2d8c593c9404ee5ad141ba414a837
  Merge pull request #1424 from CakeML/bvi-multiret-fix
HOL:d456022724bd61e57303339e998313b6580c592d
  build_help: derive sibling/stem manuals from Manual/mdbook.mk
Machine:lammmington

 Claimed job
 Reusing HOL
 Starting developers
 FAILED: developers
Starting work on lint_build_dirs
lint_build_dirs                                                     (0s)     OK
Starting work on lint
readme_gen                                                          (1s)     OK
Starting work on README.md
README.md                                                           (0s)FAIL<1>
lint                                                                (0s) killed
*** Holmake aborted - 1 target failed:
*** README.md (status 1)
 Checking: /scratch/cakeml/regression3/cakeml-3407
 ERROR! Every Holmakefile must include a README.md target. Consider adding:
 
 INCLUDES =
 
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all
 
 README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
 DIRS = $(wildcard */)
 README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
 	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
 
 to /scratch/cakeml/regression3/cakeml-3407/Holmakefile
 
 Full log: /scratch/cakeml/regression3/cakeml-3407/developers/.hol/logs/README.md