Even more attempts

README.md

@@ -15,20 +15,20 @@ See the `version1` branch for the previous version.
 Directory structure
 -------------------
 
-[COPYING](COPYING): 
+[](COPYING):
 CakeML Copyright Notice, License, and Disclaimer.
 
-[build-instructions.sh](build-instructions.sh): 
+[](build-instructions.sh):
 This script installs Poly/ML, HOL and CakeML.
 
-[developers](developers): 
+[](developers):
 This directory contains scripts for automating routine tasks, e.g. for
 running regression tests.
 
-[miscScript.sml](miscScript.sml): 
+[](miscScript.sml):
 Miscellaneous definitions and minor lemmas used throughout the
 development.
 
-[mlstringScript.sml](mlstringScript.sml): 
+[](mlstringScript.sml):
 Small theory of wrapped strings, so the translator can distinguish
 them from char lists and can target CakeML strings directly.

developers/README.md

@@ -1,36 +1,36 @@
 This directory contains scripts for automating routine tasks, e.g. for
 running regression tests.
 
-[build-email.sh](build-email.sh): 
+[](build-email.sh):
 This script produces a report on whether a regression test
 succeeded, timed out or failed.
 
-[build-sequence](build-sequence): 
+[](build-sequence):
 The regression test runs through this list of directories.
 
-[build-travis.sh](build-travis.sh): 
+[](build-travis.sh):
 A Travis selftest script. This file is probably obsolete, since
 Travis is no longer supported.
 
-[cached-deps.sh](cached-deps.sh): 
+[](cached-deps.sh):
 A script for downloading cached state for Travis. This file is
 probably obsolete, since Travis is no longer supported.
 
-[install-deps.sh](install-deps.sh): 
+[](install-deps.sh):
 Builds various things for Travis. This file is probably obsolete,
 since Travis is no longer supported.
 
-[misc.sh](misc.sh): 
+[](misc.sh):
 Functions for displaying time and memory usage.
 
-[readme_gen.sml](readme_gen.sml): 
+[](readme_gen.sml):
 This SML program generates a `README.md` summary for the files
 given as command-line arguments to this script. The contents of the
 summaries are read from a specific style of comment that needs to
 appear at the top of each given file.
 
-[regression-test.sh](regression-test.sh): 
+[](regression-test.sh):
 A script that runs the regression test.
 
-[wc.sh](wc.sh): 
+[](wc.sh):
 A script that counts non-blank lines.

developers/readme_gen.sml

@@ -248,7 +248,7 @@ fun create_summary filenames = let
   fun write_item (Prefix lines) = (map write_line lines; ())
     | write_item (Error _) = ()
     | write_item (TitleAndContent (title,lines)) =
-        (write_line ("\n[](" ^ title ^ ") — \n") ;
+        (write_line ("\n[](" ^ title ^ "):\n") ;
          map write_line lines; ())
   val _ = map write_item output
   val _ = TextIO.closeOut(f)