diff options
Diffstat (limited to 'parsing/printmod.ml')
| -rw-r--r-- | parsing/printmod.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index cf2aad203..9cf76585e 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -28,6 +28,7 @@ let short = ref false let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; |