diff options
| author | Enrico Tassi | 2014-10-31 14:43:04 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-31 15:54:00 +0100 |
| commit | baef2bd34e1906ab56918c37a90c5468a4785656 (patch) | |
| tree | dda40ffcff58cedeacc45ae6d79fda6e0774e3e2 /dev | |
| parent | b4c8a7ead01ac81575530e36386a58f49432b35f (diff) | |
Show_script called only if in coqtop mode
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions