Merge branch 'master' into multiple_wms

wrench-project · Feb 14, 2018 · 0a7a796 · 0a7a796
2 parents 92529dc + 9b71032
commit 0a7a796
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.travis.yml b/.travis.yml
@@ -32,7 +32,7 @@ before_install:
       docker exec -it wrench git clone https://github.com/wrench-project/wrench;
     fi
   - if [[ "$BRANCH" != "HEAD" ]]; then
-      docker exec -w /home/wrench/wrench -it wrench git checkout ${BRANCH}
+      docker exec -w /home/wrench/wrench -it wrench git checkout ${BRANCH};
     fi
   - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
       docker exec -it wrench mkdir wrench/build;