diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-10 08:50:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-10 08:50:16 +0200 |
| commit | 7b32d8454ded5497d677d5dbcc665aacb6725e6b (patch) | |
| tree | cc0c2c76eda49943edd452cffd3e0d9de3606bb7 /pretyping/redops.mli | |
| parent | f3f387e63789def93219f407bb2a35257143b73d (diff) | |
| parent | e95b816ed34a379e6b6f38630e416710d66c4179 (diff) | |
Merge PR#547: [toplevel] Remove the feedback printer only on exit.
Diffstat (limited to 'pretyping/redops.mli')
0 files changed, 0 insertions, 0 deletions