Skip to content

Commit 313e65f

Browse files
fingolfinjames-d-mitchell
authored andcommitted
doc: specify full main XML filename
For historical reasons, AutoDoc allows omitting the file extensions, but this is an undocumented feature. So better not to rely on it.
1 parent 423ceee commit 313e65f

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

makedoc.g

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ AutoDoc("digraphs", rec(
127127
\usepackage{a4wide}
128128
\newcommand{\bbZ}{\mathbb{Z}}
129129
"""),
130-
main := "main",
130+
main := "main.xml",
131131
files := Files),
132132

133133
scaffold := rec(

0 commit comments

Comments
 (0)