diff options
| author | Pierre-Marie Pédrot | 2014-04-25 14:36:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:39:15 +0200 |
| commit | 38d2881dcd1917a93b202c16a55d57d51006ee88 (patch) | |
| tree | c3995446d077b16a55367e52af4d45013707b805 /dev/db | |
| parent | b35edb34769fecd4dbdf7030222ba3078eab1c93 (diff) | |
Adding a debug printer for futures.
Diffstat (limited to 'dev/db')
| -rw-r--r-- | dev/db | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -2,6 +2,8 @@ load_printer "gramlib.cma" load_printer "str.cma" load_printer "printers.cma" +install_printer Top_printers.ppfuture + install_printer Top_printers.ppid install_printer Top_printers.ppidset install_printer Top_printers.ppevar |