CakeML:3da61f257e361e9876320af1b4798f088e41ac95
Merge with latest changes from master
#865 (Iced_cake)
Merging into:26a8781cbc72e741e00c013f73ad90b079fd422d
Merge pull request #863 from CakeML/repl
HOL:9ef02c741e59da2e5b90512fc92aa8194c043623
Fix Holmakefiles for Tamarack example; further modernise port-full
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
FAILED: developers
readme_gen (0s) OK
Starting work on README.md
README.md (2s)FAIL<1>
Checking: /home/cug/hk324/cml-regression/cakeml-1816/compiler/bootstrap/compilation/ag32/32/proofs
Checking: /home/cug/hk324/cml-regression/cakeml-1816/compiler/bootstrap/translation
Checking: /home/cug/hk324/cml-regression/cakeml-1816/compiler/proofs
Checking: /home/cug/hk324/cml-regression/cakeml-1816/tutorial
Checking: /home/cug/hk324/cml-regression/cakeml-1816/tutorial/solutions
Checking: /home/cug/hk324/cml-regression/cakeml-1816/icing
Checking: /home/cug/hk324/cml-regression/cakeml-1816/icing/examples
File not allowed to exist: /home/cug/hk324/cml-regression/cakeml-1816/icing/examples/output/readmePrefix
Such files are only allowed in directories with a Holmakefile.
Fix: rename the file to README.md