diff options
| author | Enrico Tassi | 2014-09-16 16:57:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-16 17:34:57 +0200 |
| commit | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch) | |
| tree | 2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /plugins/funind | |
| parent | 26aa224293e88611dcb543e400488013bc8b30b4 (diff) | |
Undo prints only if coqtop || emacs
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions