fix PATH in configuration

instead of writing the current PATH, write "$PATH" by escaping it.

diff --git a/deal.II-toolchain/packages/git.package b/deal.II-toolchain/packages/git.package
index 93a5f2c1a756f7c9af272e592a7aad180f28811f..48d496b5ef63de1d12b90e33522b60ff89e5b300 100644 (file)
--- a/deal.II-toolchain/packages/git.package
+++ b/deal.II-toolchain/packages/git.package
@@ -26,6 +26,6 @@ package_specific_conf () {
     CONFIG_FILE=${CONFIGURATION_PATH}/${NAME}
     rm -f $CONFIG_FILE
     echo "
-export PATH=${INSTALL_PATH}/bin:$PATH
+export PATH=${INSTALL_PATH}/bin:\${PATH}
 " >> $CONFIG_FILE
 }

diff --git a/deal.II-toolchain/packages/numdiff.package b/deal.II-toolchain/packages/numdiff.package
index 72fc4abab1e090d904ada656a80db5b929887b39..aa288dd43e258112598331971790523c56d8fcb9 100644 (file)
--- a/deal.II-toolchain/packages/numdiff.package
+++ b/deal.II-toolchain/packages/numdiff.package
@@ -18,6 +18,6 @@ package_specific_conf () {
     CONFIG_FILE=${CONFIGURATION_PATH}/${NAME}
     rm -f $CONFIG_FILE
     echo "
-export PATH=${INSTALL_PATH}:$PATH
+export PATH=${INSTALL_PATH}:\${PATH}
 " >> $CONFIG_FILE
 }