diff options
| -rw-r--r-- | docs/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/docs/Makefile b/docs/Makefile index e685704bea..86b5d8f1b1 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -47,4 +47,5 @@ ps/%.ps: %.dvi html/%/index.html: src/%.tex mkdir -p html/$* latex2html -split 0 -show_section_numbers -toc_depth 3 -nonavigation \ - -noinfo -math -dir html/$* $< 1>/dev/null 2>/dev/null + -numbered_footnotes -local_icons -noinfo -math -dir html/$* \ + $< 1>/dev/null 2>/dev/null |