projects
/
projects.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
1b1a4b9
)
epic
author
Michael Wagner
<mail@wagnertech.de>
Sat, 9 Dec 2017 21:05:06 +0000
(22:05 +0100)
committer
Michael Wagner
<mail@wagnertech.de>
Sat, 9 Dec 2017 21:05:06 +0000
(22:05 +0100)
tools/make/configure
patch
|
blob
|
history
diff --git
a/tools/make/configure
b/tools/make/configure
index
47a1304
..
4a1349a
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