aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_include
diff options
context:
space:
mode:
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include
index 2a4ad4a15..472c0c605 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -52,7 +52,7 @@
#install_printer ppvblock;;
#install_printer (* bigint *) ppbigint;;
#install_printer (* loc *) pploc;;
-#install_printer (* substitution *) prsubst;;
+#install_printer (* substitution *) ppsubst;;
(* Open main files *)