From 81896bcf80425cf33789528885e3ff90cc53de54 Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@sophia.inria.fr>
Date: Wed, 26 Jan 2011 09:26:53 +0100
Subject: [PATCH] trash lock file if older than 2h

---
 scripts/all-modules.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/scripts/all-modules.sh b/scripts/all-modules.sh
index b33276e..94a0246 100755
--- a/scripts/all-modules.sh
+++ b/scripts/all-modules.sh
@@ -86,6 +86,15 @@ function main () {
 	shift
     done
 
+    # is the stamp older than 2 hours ? 
+    # in minutes
+    GRACE=120
+    is_old=$(find $LOCK -mmin +$GRACE 2> /dev/null)
+    if [ -n "$is_old" ] ; then
+	echo "$LOCK is older than $GRACE minutes - removing"
+	rm -f $LOCK
+    fi
+
     [ -f $LOCK ] && exit 1
     
     echo $$ > $LOCK
-- 
2.43.0