Merge branch 'master' of github.com:mininet/mininet

2013-12-12 15:56:41 -08:00
parent 49994c8915 17dbc7e055
commit 50423936b2
7 changed files with 9 additions and 10 deletions
@@ -8,7 +8,7 @@ version = 'Mininet ' + co( 'PYTHONPATH=. bin/mn --version', shell=True )
 version = version.strip()

 # Find all Mininet path references
-lines = co( "grep -or 'Mininet \w\.\w\.\w\w*' *", shell=True )
+lines = co( "grep -or 'Mininet \w\+\.\w\+\.\w\+[+]*' *", shell=True )

 error = False