Merge pull request #98084 from turion/patch-5

agda.section.md: Fix header and enumeration
2020-10-11 07:29:58 -04:00
parent fa0df4d5ab 4336f9f7bb
commit 8b33d575e4
2 changed files with 23 additions and 18 deletions
@@ -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"
    )