Improved naming of generated HTML files by using nice IDs
authorsven.panne@aedion.de <unknown>
Wed, 7 Feb 2007 16:34:04 +0000 (16:34 +0000)
committersven.panne@aedion.de <unknown>
Wed, 7 Feb 2007 16:34:04 +0000 (16:34 +0000)
commita8e681c1e8aa4bc602714ff61583cd4e969d7187
treee65508610279a1514aceb9290f6b33585b5c7b12
parent2f4e21c6f741995e20cc3b53b109ff9edf18eb3c
Improved naming of generated HTML files by using nice IDs
15 files changed:
docs/users_guide/5-00-notes.xml
docs/users_guide/5-04-notes.xml
docs/users_guide/6.6-notes.xml
docs/users_guide/ffi-chap.xml
docs/users_guide/flags.xml
docs/users_guide/ghci.xml
docs/users_guide/glasgow_exts.xml
docs/users_guide/gone_wrong.xml
docs/users_guide/installing.xml
docs/users_guide/parallel.xml
docs/users_guide/phases.xml
docs/users_guide/runtime_control.xml
docs/users_guide/separate_compilation.xml
docs/users_guide/using.xml
docs/users_guide/win32-dlls.xml