kill a useless file

[simgrid.git] / tools / jenkins / Sanitizers.sh

diff --git a/tools/jenkins/Sanitizers.sh b/tools/jenkins/Sanitizers.sh
index 63064ba..9d83f58 100755 (executable)
--- a/tools/jenkins/Sanitizers.sh
+++ b/tools/jenkins/Sanitizers.sh
@@ -55,7 +55,7 @@ do
    fi
 done
 
-### Cleanup previous runs
+### Cleanup previous runs
 
 ! [ -z "$WORKSPACE" ] || die "No WORKSPACE"
 [ -d "$WORKSPACE" ] || die "WORKSPACE ($WORKSPACE) does not exist"