Skip to content

Commit b1f131b

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 3feffe9 commit b1f131b

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
@@ -131,7 +131,7 @@ AutoDoc("semigroups", rec(
131131
\usepackage{a4wide}
132132
\newcommand{\bbZ}{\mathbb{Z}}
133133
"""),
134-
main := "main",
134+
main := "main.xml",
135135
files := Files),
136136

137137
scaffold := rec(

0 commit comments

Comments
 (0)