diff options
| author | Enrico Tassi | 2021-01-06 18:21:55 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | d414273bbd53681baecf3ddc6d343243c80e8103 (patch) | |
| tree | 190a40cbc6f423865bc14bed8f471b6bc4014fd8 /dev/core.dbg | |
| parent | 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 (diff) | |
[coqargs] use standard option injection for -print-emacs
Diffstat (limited to 'dev/core.dbg')
0 files changed, 0 insertions, 0 deletions