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 /ide | |
| parent | 4f85e540349004d4f9388a90061fc4a1541d9c40 (diff) | |
[opam] Fix typo in build variable.
Fixes #8431
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 ] ] |