Skip to content

Commit

Permalink
module header is proper Rust comment
Browse files Browse the repository at this point in the history
  • Loading branch information
lemastero committed Dec 14, 2023
1 parent 0a6d976 commit c933d1b
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/Agda/Compiler/Rust/Backend.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,4 +95,4 @@ writeModule opts _ _ mName cdefs = do
-- TODO and change to TopLevelModuleName -> String
-- TODO ideally test using real file
moduleHeader :: String -> String
moduleHeader mName = "*** module " <> mName <> " ***\n"
moduleHeader mName = "// module " <> mName <> "\n"
2 changes: 1 addition & 1 deletion test/Hello.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
*** module test.Hello ***
// module test.Hello
Bool = Datatype {
dataPars = 0
dataIxs = 0
Expand Down
2 changes: 1 addition & 1 deletion test/RustBackendTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ testIsEnabled = TestCase

testModuleHeader :: Test
testModuleHeader = TestCase
(assertEqual "moduleHeader" (moduleHeader "foo") "*** module foo ***\n")
(assertEqual "moduleHeader" (moduleHeader "foo") "// module foo\n")

tests :: Test
tests = TestList [
Expand Down

0 comments on commit c933d1b

Please sign in to comment.