tools/Holmake/HM_Core_Cline.sml

9   fun from debug do_logging dontmakes fast help hmakefile holdir includes
16       fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
30             hmakefile help fast dontmakes do_logging debug =
33       fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
42   fun to f {debug, do_logging, dontmakes, fast, help, hmakefile, holdir,
47     f debug do_logging dontmakes fast help hmakefile holdir includes
67   help : bool,
93   help = false,
161   { help = "turn on diagnostic messages", long = ["dbg", "d"], short = "",
163   { help = "don't make this target", long = [], short = "d",
165   { help = "fast build (replace tactics w/cheat)", long = ["fast"], short = "",
167   { help = "show this message", long = ["help"], short = "h",
168     desc = mkBoolT #help },
169   { help = "use different HOLDIR", long = ["holdir"], short = "",
171   { help = "use different holmakefile", long = ["holmakefile"], short = "",
173   { help = "make session 'interactive'", long = ["interactive"], short = "i",
175   { help = "include directory", long = [], short = "I",
177   { help = "max number of parallel jobs", long = ["jobs"], short = "j",
179   { help = "try to build all targets", long = ["keep-going"], short = "k",
181   { help = "enable time logging", long = ["logging"], short = "",
183   { help = "print what would be executed", long = ["no_action"], short = "n",
185   { help = "don't use a Holmakefile", long = ["no_hmakefile"], short = "",
187   { help = "don't check which Holmake was last used", long = ["nolmbc"],
189   { help = "don't use Overlay.sml file", long = ["no_overlay"],
191   { help = "don't build recursively in INCLUDES",
193   { help = "don't quit on failure", long = ["noqof"], short = "",
195   { help = "use file as opentheory logging .uo",
197   { help = "be quieter with output", short = "q", long = ["quiet"],
206   { help = "quit on failure", short = "", long = ["qof"],
208   { help = "rebuild cached dependency files", short = "",
210   { help = "clean recursively", short = "r", long = [],
212   { help = "verbose output", short = "v", long = ["verbose"],