aboutsummaryrefslogtreecommitdiff
path: root/dev/db
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-09 16:04:15 +0200
committerHugo Herbelin2014-10-09 16:04:15 +0200
commit5eff644c658d1765ba73cd9e73c5bd7819c7d644 (patch)
tree6821466856341de55c5cc15ed73e61da45f80258 /dev/db
parent2d5b39132f4a7dd2541f95d795682089eb1c5f5e (diff)
Adding printer for named_context_val and Goal.goal in debugger.
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/db b/dev/db
index 04d300d409..c584adfe1e 100644
--- a/dev/db
+++ b/dev/db
@@ -32,11 +32,13 @@ install_printer Top_printers.ppconstraints
install_printer Top_printers.pptype
install_printer Top_printers.ppj
install_printer Top_printers.ppenv
+install_printer Top_printers.ppnamedcontextval
install_printer Top_printers.pp_stack_t
install_printer Top_printers.pp_cst_stack_t
install_printer Top_printers.ppmetas
install_printer Top_printers.ppevm
+install_printer Top_printers.ppgoalgoal
install_printer Top_printers.ppgoal
install_printer Top_printers.pphintdb