From 8110e9cbd6d70960a221c316774460f6ad6dc5e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Sep 2016 12:43:52 +0200
Subject: Adding debugging printer for Genarg.ArgT.t.

---
 dev/db | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/db')

diff --git a/dev/db b/dev/db
index 86e35a3ece..f226291d64 100644
--- a/dev/db
+++ b/dev/db
@@ -51,6 +51,7 @@ install_printer Top_printers.prsubst
 install_printer Top_printers.prdelta
 install_printer Top_printers.ppfconstr
 install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppgenargargt
 install_printer Top_printers.ppist
 install_printer Top_printers.ppconstrunderbindersidmap
 install_printer Top_printers.ppunbound_ltac_var_map
-- 
cgit v1.2.3