diff options
| author | Maxime Dénès | 2017-10-09 15:18:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 15:18:37 +0200 |
| commit | 73a858469479651cc4baf631a45a9ff1d69d0c66 (patch) | |
| tree | befde7e5f47ccdf4ab6063a58357f8aab7ace5b8 /lib/flags.ml | |
| parent | a82c30c08c7442b6bb43829d2be6a299f493ca88 (diff) | |
| parent | 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 (diff) | |
Merge PR #1086: [stm] [flags] Move document mode flags to the STM.
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 d4be81c61a..a178eb7552 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 |