aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-20 00:08:35 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-20 00:11:13 +0200
commit8bba34395e520ac606fc3efd0a875699fe968e69 (patch)
tree4e835c6a12b8a3d8790946843d094d91a6f778fb /dev/db
parent48c78b719392276b2e87be5ea368c71c01f14c85 (diff)
Better debug printers for module paths.
Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now.
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index f259b50eb..ece22b3f4 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppexistentialset
install_printer Top_printers.ppintset
install_printer Top_printers.pplab
install_printer Top_printers.ppdir
+install_printer Top_printers.ppmbid
install_printer Top_printers.ppmp
install_printer Top_printers.ppkn
install_printer Top_printers.ppcon