diff options
| author | Vincent Laporte | 2019-04-25 10:07:34 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-25 11:50:56 +0000 |
| commit | 5411b109d3a8575fdc012b51bbc418ad84dc686f (patch) | |
| tree | 462e20850e0e7a4102ce3a1ea66b6675371e981e /Makefile.ide | |
| parent | 47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff) | |
CoqIDE: fix open-file dialog on macOS
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) $@ |