changeset 2:4e4f3903643d

Look for e.g. Makefile.linux64 as well
author Chris Cannam
date Thu, 17 Jul 2014 13:05:17 +0100
parents ac47394e6503
children 695661d9dab9
files process.sh
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/process.sh	Mon Jul 14 13:47:37 2014 +0100
+++ b/process.sh	Thu Jul 17 13:05:17 2014 +0100
@@ -8,6 +8,7 @@
 ##   has valid .cat and .n3
 
 platform=linux
+bits=64
 
 configure_maybe() {
     dir="$1"
@@ -20,7 +21,7 @@
 
 find_makefile() {
     dir="$1"
-    for f in Makefile Makefile.$platform build/$platform/Makefile build/$platform/Makefile.$platform ; do
+    for f in Makefile Makefile.$platform Makefile.$platform$bits build/$platform/Makefile build/$platform/Makefile.$platform build/$platform/Makefile.$platform$bits; do
 	if [ -f "$dir/$f" ]; then
 	    echo $f
 	    break