summaryrefslogtreecommitdiff
path: root/src/main.mlton.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-23 17:59:23 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-23 17:59:23 -0400
commit5574caafb5da61e7938eec476975bf82cbf98b97 (patch)
tree767ed7f7342d56957d23eea82004fb2f2d85e032 /src/main.mlton.sml
parent32b2d196fc02ca4f9f87574e6da1ffa6c1ea12ab (diff)
cgi protocol
Diffstat (limited to 'src/main.mlton.sml')
-rw-r--r--src/main.mlton.sml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 1fd4f073..069de100 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -32,6 +32,9 @@ fun doArgs (args, (timing, demo, sources)) =
doArgs (rest, (timing, SOME (prefix, false), sources))
| "-guided-demo" :: prefix :: rest =>
doArgs (rest, (timing, SOME (prefix, true), sources))
+ | "-protocol" :: name :: rest =>
+ (Settings.setProtocol name;
+ doArgs (rest, (timing, demo, sources)))
| arg :: rest =>
let
val acc =