aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/demo.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-07-18 11:01:48 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-07-18 11:01:48 -0400
commitdddebbe923d37a5246a6727b27028e77b8252a1d (patch)
tree8bf5b15ad81f9a06146c5d0a4895492dcd9fc8d0 /src/demo.sml
parentfdca372b5e04a3f460fb3a635076b0fb81a492e7 (diff)
More command-line options
Diffstat (limited to 'src/demo.sml')
-rw-r--r--src/demo.sml12
1 files changed, 8 insertions, 4 deletions
diff --git a/src/demo.sml b/src/demo.sml
index b8323993..ebdf4e40 100644
--- a/src/demo.sml
+++ b/src/demo.sml
@@ -88,10 +88,14 @@ fun make {prefix, dirname, guided} =
else
files @ [file])
(#sources combined) (#sources urp),
- exe = OS.Path.joinDirFile {dir = dirname,
- file = "demo.exe"},
- sql = SOME (OS.Path.joinDirFile {dir = dirname,
- file = "demo.sql"}),
+ exe = case Settings.getExe () of
+ NONE => OS.Path.joinDirFile {dir = dirname,
+ file = "demo.exe"}
+ | SOME s => s,
+ sql = SOME (case Settings.getSql () of
+ NONE => OS.Path.joinDirFile {dir = dirname,
+ file = "demo.sql"}
+ | SOME s => s),
debug = Settings.getDebug (),
timeout = Int.max (#timeout combined, #timeout urp),
profile = false,