File tree Expand file tree Collapse file tree 2 files changed +5
-2
lines changed
Expand file tree Collapse file tree 2 files changed +5
-2
lines changed Original file line number Diff line number Diff line change @@ -13,7 +13,8 @@ C=$(docker container create --rm -w $W ghcr.io/codewars/lean:latest lean test/So
1313# src/Solution.lean
1414# src/Preloaded.lean
1515# test/SolutionTest.lean
16- docker container cp ./. $C :$W
16+ docker container cp src $C :$W
17+ docker container cp test $C :$W
1718
1819# Run tests
1920docker container start --attach $C
Original file line number Diff line number Diff line change 11W=/workspace/
22# Create container
33C=$(docker container create --rm -w $W ghcr.io/codewars/lean:latest lean test/SolutionTest.lean)
4+ # C=$(docker container create --rm -w $W cw_lean lean test/SolutionTest.lean)
45
56# Copy files from the current directory
67# src/Solution.lean
78# src/Preloaded.lean
89# test/SolutionTest.lean
9- docker container cp ./. $C:$W
10+ docker container cp src $C:$W
11+ docker container cp test $C:$W
1012
1113# Run tests
1214docker container start --attach $C
You can’t perform that action at this time.
0 commit comments