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
commitdddebbe923d37a5246a6727b27028e77b8252a1d (patch)
tree8bf5b15ad81f9a06146c5d0a4895492dcd9fc8d0 /src/settings.sig
parentfdca372b5e04a3f460fb3a635076b0fb81a492e7 (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