diff options
Diffstat (limited to 'src/c_backend.mli')
| -rw-r--r-- | src/c_backend.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/c_backend.mli b/src/c_backend.mli index 24f6e03b..9782f24f 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -59,6 +59,15 @@ val opt_trace : bool ref val opt_static : bool ref val opt_no_main : bool ref +(** [opt_memo_cache] will store the compiled function definitions in + file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the + original function to be compiled. Enabled using the -memo + flag. Uses Marshal so it's quite picky about the exact version of + the Sail version. This cache can obviously become stale if the C + backend changes - it'll load an old version compiled without said + changes. *) +val opt_memo_cache : bool ref + (** Optimization flags *) val optimize_primops : bool ref |