Merge necessary to resync branch 'dev' after commit of verus bash file with error

2018-05-15 00:50:28 -07:00
parent 7702587db8 72c5a7d56f
commit 3789cb0885
1 changed files with 6 additions and 1 deletions
--- a/src/fiat/verus
+++ b/src/fiat/verus
@@ -1,2 +1,7 @@
 #!/bin/bash
-./komodo-cli -ac_name=VERUSTEST "$@"
+
+#set working directory to the location of this script
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+cd $DIR
+
+../komodo-cli -ac_name=VERUSTEST "$@"