diff options
| author | Enrico Tassi | 2017-08-04 16:51:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-04 16:51:30 +0200 |
| commit | 7a14df13a771651973da980eb9ab5c6608ffdcef (patch) | |
| tree | a7d26c7642f65c599b4ea6ea8800ff8bce85d2a9 /API | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) | |
Makefile: install-byte works even if -coqide no
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions