Merge branch 'master' into 'master'

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

diff --git a/tools/jenkins/project_description.sh b/tools/jenkins/project_description.sh
index 87b827488f53eb46408ff1ed7d9d22339c690db4..eb77ba6bfffc5f7eb58f254968599fc63bcb49b8 100755 (executable)
--- a/tools/jenkins/project_description.sh
+++ b/tools/jenkins/project_description.sh
@@ -26,7 +26,7 @@ get_eigen3(){
 }
 
 get_ns3(){
-  grep -m 1 "ns-3 found (v3.[0-9]*; incl:" ./consoleText | sed "s/.*-- ns-3 found .v\(3.[0-9]*\); incl:.*/\1/g"
+  grep -m 1 "ns-3 found (v3.[0-9dev]*; incl:" ./consoleText | sed "s/.*-- ns-3 found .v\(3.[0-9dev]*\); incl:.*/\1/g"
 }
 
 get_python(){