aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorEnrico Tassi2015-01-06 18:09:26 +0100
committerEnrico Tassi2015-01-06 18:09:35 +0100
commit341909bbc5c1c59e81dfad2f2532602e2561ec36 (patch)
tree28fb527cb921b4e02d4722549a24f6e2366f5c76 /lib/flags.ml
parentbf16900f43c1291136673e7614587fe51eebc88f (diff)
rename: vi -> vio
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 9c718743d2..ad69c5a2b9 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,7 @@ let boot = ref false
let load_init = ref true
let batch_mode = ref false
-type compilation_mode = BuildVo | BuildVi | Vi2Vo
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
let compilation_mode = ref BuildVo
type async_proofs = APoff | APonLazy | APon