diff options
| author | Enrico Tassi | 2014-10-06 08:53:23 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-06 08:53:23 +0200 |
| commit | b770451a4b3c74db78457951f75505b53d362c12 (patch) | |
| tree | 162199758b76f573db9b4da5d73b9df440c58ab9 /dev/include | |
| parent | 6adbf7d9678257aa42ef0d3b30db2e484cd148ad (diff) | |
fix wrong escaping in coq_makefile
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions