diff options
| author | Emilio Jesus Gallego Arias | 2018-09-10 10:46:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-20 20:06:36 +0200 |
| commit | 8f23d8d339403006d6464510c7d2cd285cf38b0a (patch) | |
| tree | ababa334c4d40f0386be7ac235eb7b4acae0be6d | |
| parent | 4f85e540349004d4f9388a90061fc4a1541d9c40 (diff) | |
[opam] Fix typo in build variable.
Fixes #8431
| -rw-r--r-- | coq.opam | 2 | ||||
| -rw-r--r-- | ide/coqide.opam | 2 |
2 files changed, 2 insertions, 2 deletions
@@ -18,5 +18,5 @@ depends: [ build: [ [ "dune" "build" "@vodeps" ] [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] - [ "dune" "build" "-p" package "-j" jobs ] + [ "dune" "build" "-p" name "-j" jobs ] ] 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 ] ] |