diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2018-12-14 15:42:59 -0500 |
| commit | c1932084390aca19c748da024b7b168c160a3aea (patch) | |
| tree | 9a9865eda9aed3d1127eecb332ec799bd8d051cd /src/settings.sig | |
| parent | 720e1cb2c84dfd274fcbfd7bf4974a1c110501cb (diff) | |
New .urp option: safeGetDefault
Diffstat (limited to 'src/settings.sig')
| -rw-r--r-- | src/settings.sig | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig index 986d6ed7..6ba7e96a 100644 --- a/src/settings.sig +++ b/src/settings.sig @@ -258,6 +258,7 @@ signature SETTINGS = sig val getFileCache : unit -> string option (* Which GET-able functions should be allowed to have side effects? *) + val setSafeGetDefault : bool -> unit val setSafeGets : string list -> unit val isSafeGet : string -> bool |