aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-23 12:23:06 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-11-23 13:38:29 +0100
commit9aae44e9c63d4833bf644b21e0ca7d8adab92e3a (patch)
tree896bf4b0485f5d7d87e373135aa6a41e1457e4cf /dev/db
parentb3b3bbe6a0c0693c2a4e154685d109282d4b6f07 (diff)
Add printer for transparent state for ocamldebug.
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 8588f6272..d7131757a 100644
--- a/dev/db
+++ b/dev/db
@@ -22,6 +22,7 @@ install_printer Top_printers.ppsp
install_printer Top_printers.ppqualid
install_printer Top_printers.ppclindex
install_printer Top_printers.ppbigint
+install_printer Top_printers.pp_transparent_state
install_printer Top_printers.pppattern
install_printer Top_printers.ppglob_constr