diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index b7be2c0f5..7dd59cf05 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -18,7 +18,7 @@ open Goptions - The "short" one, that just prints the names of the fields. - The "rich" one, that also tries to print the types of the fields. The short version used to be the default behavior, but now we print - types by default. The following option allows to change this. + types by default. The following option allows changing this. Technically, the environments in this file are either None in the "short" mode or (Some env) in the "rich" one. *) |