diff options
Diffstat (limited to 'patch-Makefile')
| -rw-r--r-- | patch-Makefile | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/patch-Makefile b/patch-Makefile new file mode 100644 index 000000000000..c3c9f4ecb91e --- /dev/null +++ b/patch-Makefile @@ -0,0 +1,19 @@ +*** Makefile 2016-06-04 10:59:52.438996452 +1000 +--- Makefile-new 2016-06-04 11:00:02.238996854 +1000 +*************** +*** 68,74 **** + ifeq (${WITH_GTK},yes) + ${GPRINSTALL} ${GPRINST_OPTS} -Psrc/gnatcoll_gtk + endif +! ${GPRINSTALL} --mode=usage ${GPRINST_OPTS} -Psrc/gnatcoll_tools + + install_gps_plugin: force + mkdir -p $(prefix)/share/gps/plug-ins +--- 68,74 ---- + ifeq (${WITH_GTK},yes) + ${GPRINSTALL} ${GPRINST_OPTS} -Psrc/gnatcoll_gtk + endif +! # ${GPRINSTALL} --mode=usage ${GPRINST_OPTS} -Psrc/gnatcoll_tools + + install_gps_plugin: force + mkdir -p $(prefix)/share/gps/plug-ins |