| commit | 8f9d062efb013825c03ef0cae89839edbeb4b4fe | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davide.pesavento@lip6.fr> | Tue Nov 27 01:23:37 2018 -0500 |
| committer | Davide Pesavento <davide.pesavento@lip6.fr> | Tue Nov 27 01:45:53 2018 -0500 |
| tree | fdc5e45c84eef2e3d0f74a3ac8f905dfdf0d43c9 | |
| parent | e41e71e830ba81f8ddcf99285982560a139cc6d5 [diff] [blame] |
Update build flags, Jenkins scripts, and Travis configuration Change-Id: I738e9a9cd21be6c94e1ae3f646c959cdb89ab6f0
diff --git a/.jenkins b/.jenkins index 03d67b3..674d751 100755 --- a/.jenkins +++ b/.jenkins
@@ -7,4 +7,4 @@ [[ -f $file && -x $file ]] || continue echo "Run: $file" "$file" -done \ No newline at end of file +done