diff options
| author | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
| commit | 508265318ad39d2962587af4e10f79f4cf4cf4c6 (patch) | |
| tree | d4a32174d207668881e3de350863764760541f5f /ide | |
| parent | 80b0619e81bec85e8f37b4ee9f8e4d5faa3eae13 (diff) | |
| parent | 81e4c7152da598c1750e7881b197a6fcf54e818d (diff) | |
Merge PR #8443: [opam] [dune] Fix typo + set prefix for configure.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.opam | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.opam b/ide/coqide.opam index 1b46efdee2..ba05b9edcf 100644 --- a/ide/coqide.opam +++ b/ide/coqide.opam @@ -16,4 +16,4 @@ depends: [ "coq" ] -build: [ [ "dune" "build" "-p" package "-j" jobs ] ] +build: [ [ "dune" "build" "-p" name "-j" jobs ] ] |