diff --git a/docs/cmu-user/Makefile b/docs/cmu-user/Makefile index 5cc85238eabc1c61462a08fb5e4fb616fde99470..7ec1c8d4c6bbed5f80f5eb533c415f74e1383814 100644 --- a/docs/cmu-user/Makefile +++ b/docs/cmu-user/Makefile @@ -20,7 +20,8 @@ # generated using the Hevea tool, which is available from # <URL:http://pauillac.inria.fr/~maranget/hevea/>. The HTML files are # then split into sections using the hacha tool (distributed with -# hevea), and cleaned up using tidy. +# hevea), and cleaned up using tidy. Note that hevea 1.10 produces +# HTML that looks a bit weird. However, hevea 1.06 works nicely. # # The generated DVI file should include clickable hyperlinks. The PDF # output should include a hyperlinked table of contents, hyperlinked