diff options
Diffstat (limited to 'Makefile.ide')
| -rw-r--r-- | Makefile.ide | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.ide b/Makefile.ide index 8f9088a04a..c580bbc680 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -255,6 +255,8 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/ cp -R "$(GTKSHARE)/"locale $@ cp -R "$(GTKSHARE)/"themes $@ + $(MKDIR) $@/glib-2.0/schemas + glib-compile-schemas --targetdir=$@/glib-2.0/schemas "$(GTKSHARE)/"glib-2.0/schemas/ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(MKDIR) $@ |