diff options
| author | Enrico Tassi | 2014-10-07 11:40:45 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-07 11:41:44 +0200 |
| commit | d6851cb4ee7d351159f0e3706574b8e384e10650 (patch) | |
| tree | a5dfb7ec605039304f5d209ced7f5566e8d31d76 /dev | |
| parent | 24f5b8cf170012d43c00d5340173463438905ad2 (diff) | |
coq_makefile: explicit target install-toploop for toploop plugins
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions