forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
"make world" and dune default target don't build coqide
makefile: add coqide target The current behaviour seems mostly annoying to those who don't care about coqide.
- Loading branch information
1 parent
c87f90a
commit 6752d5b
Showing
4 changed files
with
17 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
5 changes: 5 additions & 0 deletions
5
doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
- **Changed:** | ||
when building Coq, the makefile's `world` target and `dune build`'s default target do not build coqide anymore. | ||
Use `make world coqide` or `dune build @default coqide.install` to build what they respectively used to build | ||
(`#19378 <https://github.com/coq/coq/pull/19378>`_, | ||
by Gaëtan Gilbert). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters