diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index aa98d5e19c..508776f3ba 100644 --- a/Makefile.build +++ b/Makefile.build @@ -303,7 +303,7 @@ COQIDEFLAGS=-thread $(COQIDEINCLUDES) .SUFFIXES:.vo -IDEFILES=ide/coq.png ide/.coqide-gtk2rc +IDEFILES=ide/coq.png ide/coqide-gtk2rc coqide-binaries: coqide-$(HASCOQIDE) coqide-no: |