Merge ../projects

[projects.git] / tools / make / configure

diff --git a/tools/make/configure b/tools/make/configure
index e91b31ad2110bd3bd9ff0aa1006b1160c3a26c3e..a92ecbd7e017e19861e06092c2e24bf29f9ae528 100755 (executable)
--- a/tools/make/configure
+++ b/tools/make/configure
@@ -130,6 +130,11 @@ then
 project = $paket
 COPY = ./$paket.cp
 MAKE_PRE
+       if [ -n "$ARCH" ]
+       then
+               echo "arch = $ARCH" >>make.pre
+               echo "_arch = _${ARCH}" >>make.pre
+       fi
        echo "make.pre written."
 fi