From f7c19e44e7ce35a73a3b4a95bf486d1fdb96e555 Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Tue, 16 Apr 2013 22:07:18 +0200
Subject: [PATCH] Improved patch script.
It is more flexible since it allows adding new files instead of just patching
---
patches/patch.sh | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/patches/patch.sh b/patches/patch.sh
index 08f4a852b..082026b24 100755
--- a/patches/patch.sh
+++ b/patches/patch.sh
@@ -157,6 +157,10 @@ if [ -z "$config" ]
then
config="$PLUMED_ROOT/patches/${engine}.config"
fi
+if [ -z "$otherfiles" ]
+then
+ test -d "$PLUMED_ROOT/patches/${engine}" && otherfiles="$PLUMED_ROOT/patches/${engine}/"
+fi
echo "MD engine: $engine"
echo "PLUMED location: $PLUMED_ROOT"
@@ -168,6 +172,11 @@ then
source "$config"
fi
+if [ -d "$otherfiles" ]
+then
+ echo "extra files located in: $otherfiles"
+fi
+
case "$mode" in
(static|shared|runtime) ;;
(*)
--
GitLab