diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 85bb287c22..a5fd7f69ed 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -44,7 +44,6 @@ let short = ref false let () = declare_bool_option { optdepr = false; - optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; optwrite = ((:=) short) } |