From dddebbe923d37a5246a6727b27028e77b8252a1d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 18 Jul 2009 11:01:48 -0400 Subject: More command-line options --- src/demo.sml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'src/demo.sml') 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, -- cgit v1.2.3