diff options
Diffstat (limited to 'src/c_backend.mli')
| -rw-r--r-- | src/c_backend.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/c_backend.mli b/src/c_backend.mli index 6e175ad7..170c5bd9 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -56,6 +56,7 @@ open Type_check val opt_ddump_flow_graphs : bool ref val opt_trace : bool ref val opt_static : bool ref +val opt_no_main : bool ref (** Optimization flags *) |