summaryrefslogtreecommitdiff
path: root/driver/optmain.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/optmain.ml')
-rw-r--r--driver/optmain.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/optmain.ml b/driver/optmain.ml
index 90e1cd679f..13b6000c70 100644
--- a/driver/optmain.ml
+++ b/driver/optmain.ml
@@ -132,6 +132,7 @@ module Options = Main_args.Make_optcomp_options (struct
let _pp s = preprocessor := Some s
let _ppx s = ppx := s :: !ppx
let _principal = set principal
+ let _short_paths = clear real_paths
let _rectypes = set recursive_types
let _runtime_variant s = runtime_variant := s
let _strict_sequence = set strict_sequence