tests/agda: Fix comment
This commit is contained in:
@@ -31,7 +31,7 @@ in
|
||||
machine.succeed('echo "import IO" > TestIO.agda')
|
||||
machine.succeed("agda -l standard-library -i . TestIO.agda")
|
||||
|
||||
# # Hello world
|
||||
# Hello world
|
||||
machine.succeed(
|
||||
"cp ${hello-world} HelloWorld.agda"
|
||||
)
|
||||
|
||||
Reference in New Issue
Block a user