diff options
| author | Enrico Tassi | 2018-05-09 14:22:18 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-05-09 18:30:58 +0200 |
| commit | 73e91542293af304ff25db9d3ea5495a9aa95249 (patch) | |
| tree | 6cc38a97dc02eb30152c4d3ba4d6e6483a1fdfa6 /dev | |
| parent | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (diff) | |
test for coqc -o
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions