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/compiler.sig | |
| parent | 720e1cb2c84dfd274fcbfd7bf4974a1c110501cb (diff) | |
New .urp option: safeGetDefault
Diffstat (limited to 'src/compiler.sig')
| -rw-r--r-- | src/compiler.sig | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/compiler.sig b/src/compiler.sig index bcf69fd4..7922393d 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -61,6 +61,7 @@ signature COMPILER = sig dbms : string option, sigFile : string option, fileCache : string option, + safeGetDefault : bool, safeGets : string list, onError : (string * string list * string) option, minHeap : int, |