diff options
| author | Maxime Dénès | 2017-08-16 09:41:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:41:53 +0200 |
| commit | ae827f670d8ea405ed06b52ad841cf690ebd18a8 (patch) | |
| tree | 42f2cc914fa780416cc095e0b335c68c8eccabd6 /tools | |
| parent | ffd6a20eb807cdd381d511e7b59799495122591d (diff) | |
| parent | 7a14df13a771651973da980eb9ab5c6608ffdcef (diff) | |
Merge PR #951: Makefile: install-byte works even if -coqide no
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions