Merge pull request #17 from fingolfin/mh/fix-makedoc

Fix makedoc.g
nathancarter · Aug 11, 2022 · b9f9c6c · b9f9c6c
2 parents c0aed39 + a13ce05
commit b9f9c6c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/makedoc.g b/makedoc.g
@@ -7,6 +7,7 @@ fi;
 
 AutoDoc(
     rec(
+        scaffold := true,
         gapdoc := rec(
             LaTeXOptions := rec(
                 EarlyExtraPreamble := "\\usepackage[pdftex]{graphicx}"