Improved patch script.

It is more flexible since it allows adding new files instead of just patching

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) ;;
 (*)