From d1111c172b654efc23abc6d36cfc9e07fac28c0c Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Tue, 5 Feb 2013 15:42:01 +0100
Subject: [PATCH] Patched files are sorted

Avoid clashes between same patch created by different people
---
 patches/patch.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/patches/patch.sh b/patches/patch.sh
index 31d685abc..f21f7c034 100755
--- a/patches/patch.sh
+++ b/patches/patch.sh
@@ -223,7 +223,7 @@ case "$action" in
       echo "ERROR: I cannot find Plumed.h and Plumed.inc files. You have likely not patched yet."
       exit
     fi
-    PREPLUMED=$(find . -name "*.preplumed")
+    PREPLUMED=$(find . -name "*.preplumed" | sort)
     if ! test "$PREPLUMED" ; then
       echo "ERROR: I cannot find any .preplumed file. You have likely not patched yet."
       exit
-- 
GitLab