diff options
Diffstat (limited to 'ide/minilib.ml')
| -rw-r--r-- | ide/minilib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml index 2b278fac6..572222c06 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -20,7 +20,7 @@ type level = [ | `FATAL ] (** Some excerpt of Util and similar files to avoid loading the whole - module and its dependencies (and hence Compat and Camlp4) *) + module and its dependencies (and hence Compat and Camlp5) *) let debug = ref false |