summaryrefslogtreecommitdiff
path: root/src/settings.sig
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
commit0a58a23ed5b12a7fd128549ec430b07130453410 (patch)
tree8bf5b15ad81f9a06146c5d0a4895492dcd9fc8d0 /src/settings.sig
parent44729d96795768c87fb042f01a62e7b14469b170 (diff)
More command-line options
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index 3e8a14ac..1da58193 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -163,4 +163,13 @@ signature SETTINGS = sig
val setDbms : string -> unit
val currentDbms : unit -> dbms
+ val setDbstring : string option -> unit
+ val getDbstring : unit -> string option
+
+ val setExe : string option -> unit
+ val getExe : unit -> string option
+
+ val setSql : string option -> unit
+ val getSql : unit -> string option
+
end