diff options
author | Alexander Foremny <aforemny@posteo.de> | 2023-11-09 15:39:38 +0100 |
---|---|---|
committer | Alexander Foremny <aforemny@posteo.de> | 2023-11-09 15:39:38 +0100 |
commit | 12511580c732895e8c5d045e18803a766ed733b8 (patch) | |
tree | c13c20a9f84082d476515f5e9b19846abb12898a | |
parent | f0675acff032a2558d0d7b303c0b8199fd17c162 (diff) |
don't reference issues with @
-rw-r--r-- | app/Main.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/app/Main.hs b/app/Main.hs index e1ae560..a51ba1e 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -171,7 +171,7 @@ -- would be more appropriate? -- -- I am sympathetic to random identifiers, cf. --- @should-automatically-generated-ids-be-random, as long as they are an +-- should-automatically-generated-ids-be-random, as long as they are an -- additional mechanisam (so that we can ditch them, should they not work out). -- TODO Only separate generated tags with a blank line when description does not end with tags |