diff options
| -rw-r--r-- | docs/code.js | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/docs/code.js b/docs/code.js index a00818e..c07fa85 100644 --- a/docs/code.js +++ b/docs/code.js @@ -69,7 +69,9 @@ const parseFile = (str) => { }); } else if ((matches = line.match(/^:time (.*)$/))) { tree.push({ kind: "time", term: parseTerm(matches[1]) }); - } else if ((matches = line.match(/^([ \t]*[^:\n#][^ ]*) (.*)$/))) { + } else if ( + (matches = line.match(/^([ \t]*(?:#[^ ]|[^:\n#])[^ ]*) (.*)$/)) + ) { tree.push({ kind: "definition", name: matches[1], |