summaryrefslogtreecommitdiff
path: root/src/settings.sig
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/settings.sig
parent32b2d196fc02ca4f9f87574e6da1ffa6c1ea12ab (diff)
cgi protocol
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/settings.sig b/src/settings.sig
index bccb2ef7..c4bcf0e1 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -93,8 +93,7 @@ signature SETTINGS = sig
}
val addProtocol : protocol -> unit
val getProtocol : string -> protocol option
-
- val setProtocol : protocol -> unit
+ val setProtocol : string -> unit
val currentProtocol : unit -> protocol
end