diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 |
3 files changed, 3 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 7dfe234aa2..38a5972e96 100644 --- a/dev/base_include +++ b/dev/base_include @@ -32,7 +32,7 @@ #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; #install_printer (* cl_index *) ppclindex;; -#install_printer (* constr *) print_pure_constr;; +#install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; #install_printer (* Idpred.t *) pp_idpred;; @@ -1,4 +1,5 @@ load_printer "gramlib.cma" +load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppid diff --git a/dev/printers.mllib b/dev/printers.mllib index 2d5919d618..f93d01dafb 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -11,6 +11,7 @@ Util Bigint Hashcons Dyn +CUnix System Envars Store |