diff options
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.ide b/Makefile.ide index 8d6b5de36..c50e42341 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -62,6 +62,7 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) ########################################################################### .PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files +.PHONY: ide-toploop # target to build CoqIde coqide: coqide-files coqide-binaries theories/Init/Prelude.vo |