diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/db | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index 398f60d2b7..0b7a0b67d8 100644 --- a/dev/base_include +++ b/dev/base_include @@ -29,6 +29,7 @@ #install_printer (* qualid *) ppqualid;; #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; +#install_printer (* cl_index *) ppclindex;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; @@ -13,6 +13,7 @@ install_printer Top_printers.ppkn install_printer Top_printers.ppcon install_printer Top_printers.ppsp install_printer Top_printers.ppqualid +install_printer Top_printers.ppclindex install_printer Top_printers.ppbigint install_printer Top_printers.pppattern |