From 862214db79059e263d296920079c8d7d88c2049a Mon Sep 17 00:00:00 2001
From: Pierre
Date: Sat, 11 Jan 2014 09:22:47 +0100
Subject: 'Pretty' printer for wf_paths

---
 dev/base_include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 26ebad9662..06a62abced 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -34,6 +34,7 @@
 #install_printer  (* kernel_name *) ppkn;;
 #install_printer  (* constant *) ppcon;;
 #install_printer  (* cl_index *) ppclindex;;
+#install_printer  (* recarg Rtree.t *)  ppwf_paths;;
 #install_printer  (* constr *)  print_pure_constr;;
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
-- 
cgit v1.2.3