diff --git a/patches/patch.sh b/patches/patch.sh index 08f4a852b4a98318da34baf6d2a9a8409f71077e..082026b24f091509b1cc3c49d7fde72897bbdb64 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) ;; (*)