From 17aa50c3cdf3766cdba76ea9d82c9aaa506eaa34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Sep 2020 19:32:56 +0200
Subject: Adding debugging printers for Intmap.

---
 dev/include_printers | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/include_printers')

diff --git a/dev/include_printers b/dev/include_printers
index 30529b5fd6..7583762970 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -26,6 +26,8 @@
 #install_printer  (* judgement *) ppj;;
 #install_printer  (* id set *) ppidset;;
 #install_printer  (* int set *) ppintset;;
+#install_printer  (* id set *) ppidmapgen;;
+#install_printer  (* int set *) ppintmapgen;;
 
 #install_printer  (* Reductionops machine stack *) pp_stack_t;;
 
-- 
cgit v1.2.3