diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index d4be81c61..a178eb755 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -43,11 +43,8 @@ let with_extra_values o l f x = let boot = ref false let load_init = ref true -let batch_mode = ref false -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None +let record_aux_file = ref false let test_mode = ref false |