diff --git a/Dockerfile b/Dockerfile index 263e10f..8f20940 100644 --- a/Dockerfile +++ b/Dockerfile @@ -6,4 +6,5 @@ env PATH="$binPath:$wdir/utils:${PATH}" run rm -r ~/pintos && ln -sf $wdir ~/pintos copy checker $binPath/checker copy setOutputFrom $binPath/setOutputFrom +run expand ~ entrypoint ["checker"] diff --git a/loader.sh b/loader.sh deleted file mode 100644 index 647f4f7..0000000 --- a/loader.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/bin/sh -l - -phase=$1 - -cd /pintos -echo "Target $phase" - -docker build -f actions.Dockerfile --build-arg phase="$phase" .