diff options
| author | Maxime Dénès | 2018-10-08 19:05:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-08 19:05:33 +0200 |
| commit | d792c2bf18e68a6301f295c79c05f25738456ecf (patch) | |
| tree | 683e0900d9e77c24fc87a290d8da0ac21b076d20 | |
| parent | 2de0af56b813f2004261eb15fe22586105f3c886 (diff) | |
| parent | 6609b8b1ea9ab96dbe7b510b92bf7b5d4b81b210 (diff) | |
Merge PR #8677: [dune] Fix bad interaction among PR #8627 and #8657
| -rw-r--r-- | dune | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -18,6 +18,7 @@ (install (section lib) + (package coq) (files revision)) |