mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 18:53:42 +03:00
8 lines
119 B
Docker
8 lines
119 B
Docker
from theodus/idris2-ci-base:latest
|
|
|
|
copy . /Idris2-dev
|
|
workdir /Idris2-dev
|
|
run make idris2
|
|
run make libs
|
|
run make test
|