mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 21:23:53 +03:00
c839c98c7d
Ideally we'd have a complete incremental build in CI, but that could be a bit fiddly to set up at the moment (updating bootstrap code might make it easier). This tests that the basic facilities work, though - there's a lot can go wrong even in a small test like this, trust me, I have made those mistakes :).
5 lines
89 B
Plaintext
5 lines
89 B
Plaintext
1/2: Building Mod (Mod.idr)
|
|
2/2: Building Main (Main.idr)
|
|
Main> 10001
|
|
Main> Bye for now!
|