blob: 54bdb920dd0b27754a351c0daaa22b7270fbbaf5 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
--- plugins/platform-launcher/library/gtk/build.csh.orig Sun Jun 13 22:33:13 2004
+++ plugins/platform-launcher/library/gtk/build.csh Sun Jun 13 22:33:39 2004
@@ -72,11 +72,11 @@
# If the OS is supported (a makefile exists)
if ("$makefile" != "") then
if ("$extraArgs" != "") then
- make -f $makefile $extraArgs
+ gmake -f $makefile $extraArgs
else
echo "Building $OS launcher. Defaults: -os $DEFAULT_OS -arch $DEFAULT_OS_ARCH -ws $DEFAULT_WS"
- make -f $makefile clean
- make -f $makefile all
+ gmake -f $makefile clean
+ gmake -f $makefile all
endif
else
echo "Unknown OS ($OS) -- build aborted"
|
