2016-07-30 17:53:18 +01:00
|
|
|
#!/usr/bin/env bash
|
|
|
|
|
|
|
|
if (( $# != 1 )); then
|
|
|
|
echo "usage: `basename $0` <archive>" 1>&2
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
ARC=$1
|
|
|
|
|
|
|
|
INITDIR=`pwd`
|
2018-12-13 05:11:34 +00:00
|
|
|
|
2018-08-28 15:00:40 +01:00
|
|
|
rm -f Grid/Eigen
|
2018-08-03 21:07:58 +01:00
|
|
|
rm -rf Eigen
|
2018-07-31 00:35:17 +01:00
|
|
|
|
|
|
|
##################
|
|
|
|
#untar
|
|
|
|
##################
|
2016-07-30 17:53:18 +01:00
|
|
|
tar -xf ${ARC}
|
2018-07-31 00:35:17 +01:00
|
|
|
ARCDIR=`tar -tf ${ARC} | head -n1 | sed -e 's@/.*@@'`
|
|
|
|
|
|
|
|
###############################
|
|
|
|
# Link to a deterministic name
|
|
|
|
###############################
|
|
|
|
|
2018-08-03 21:07:58 +01:00
|
|
|
mv ${ARCDIR} Eigen
|
2018-08-28 15:00:40 +01:00
|
|
|
ln -s ${INITDIR}/Eigen/Eigen ${INITDIR}/Grid/Eigen
|
|
|
|
ln -s ${INITDIR}/Eigen/unsupported/Eigen ${INITDIR}/Grid/Eigen/unsupported
|
2018-07-31 00:35:17 +01:00
|
|
|
|
|
|
|
# Eigen source headers
|
2018-08-28 15:00:40 +01:00
|
|
|
cd ${INITDIR}/Grid
|
|
|
|
echo 'eigen_files =\' > ${INITDIR}/Grid/Eigen.inc
|
|
|
|
find -L Eigen -type f -print | sed 's/^/ /;$q;s/$/ \\/' >> ${INITDIR}/Grid/Eigen.inc
|
2018-07-31 00:35:17 +01:00
|
|
|
|
|
|
|
###################################
|
|
|
|
# back to home
|
|
|
|
###################################
|
2016-07-30 17:53:18 +01:00
|
|
|
cd ${INITDIR}
|
2018-03-20 11:18:56 +00:00
|
|
|
|