summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@csail.mit.edu>2019-01-27 09:42:40 -0500
committerGravatar GitHub <noreply@github.com>2019-01-27 09:42:40 -0500
commitbc45a4ed71477ab4374a2702f20dd45fe02c5449 (patch)
treedc9b6846676dde5158450465766f4eb6963ff932 /src/settings.sig
parent28ab84cb7b09e23aa0ed014bf2ed1fda56fcefc1 (diff)
parent949a2d6767aeec22a029c353b8a12be3665e60ec (diff)
Merge pull request #170 from ashalkhakov/endpoints
Endpoints output
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index a6a9c5fc..97d56b45 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -240,6 +240,9 @@ signature SETTINGS = sig
val setSql : string option -> unit
val getSql : unit -> string option
+ val setEndpoints : string option -> unit
+ val getEndpoints : unit -> string option
+
val setCoreInline : int -> unit
val getCoreInline : unit -> int