diff options
Diffstat (limited to 'dev/include_printers')
| -rw-r--r-- | dev/include_printers | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/include_printers b/dev/include_printers index d077075eeb..30529b5fd6 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -27,7 +27,6 @@ #install_printer (* id set *) ppidset;; #install_printer (* int set *) ppintset;; -#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; #install_printer (* Reductionops machine stack *) pp_stack_t;; (*#install_printer (* hint_db *) print_hint_db;;*) |