diff options
Diffstat (limited to 'Assignment2/src/start.sh')
-rwxr-xr-x | Assignment2/src/start.sh | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Assignment2/src/start.sh b/Assignment2/src/start.sh index b8b945d..aafbd9e 100755 --- a/Assignment2/src/start.sh +++ b/Assignment2/src/start.sh @@ -2,10 +2,7 @@ DOCKER_IMAGE=stormpy DOCKER_NAME=stormpy -docker image $DOCKER_IMAGE >/dev/null 2>&1 -if [ $? != 0 ]; then - docker build -t $DOCKER_IMAGE . -fi +docker build -q -t $DOCKER_IMAGE . docker run\ --mount type=bind,source="$PWD",target=/src\ |