Merge pull request #1 from gbenm/develop

Develop
gbenm · Oct 20, 2022 · 0931421 · 0931421
2 parents ae93e2a + 19028c5
commit 0931421
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -1,8 +1,8 @@
-from gbenm/pintos:latest
-arg wdir=/github/workspace
-arg binPath=/gbenm-actions
-workdir $wdir
-env PATH="$binPath:$binPath/utils:${PATH}"
-copy checker $binPath/checker
-copy setOutputFrom $binPath/setOutputFrom
-entrypoint ["checker"]
+FROM gbenm/pintos:latest
+ARG wdir=/github/workspace
+ARG binPath=/gbenm-actions
+WORKDIR $wdir
+ENV PATH="$binPath:$binPath/utils:${PATH}"
+COPY checker $binPath/checker
+COPY setOutputFrom $binPath/setOutputFrom
+ENTRYPOINT ["checker"]