From 87cbd64254f33439882156d9a297a6a2f6886057 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 16 Dec 2017 10:58:52 +0100
Subject: Cleanup debug printers a bit, add generated mli.

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

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 1da5e3ed18..d6c00ef5ad 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -54,7 +54,7 @@
 #install_printer ppvblock;;
 #install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
-#install_printer  (* substitution *) prsubst;;
+#install_printer  (* substitution *) ppsubst;;
 
 (* Open main files *)
 
-- 
cgit v1.2.3