Nothing but default settings is really working now:
- most formats are no longer available on MySQL formats
- for downloadable doc our links are in most cases broken and nobody
noticed this, so I assume nobody is using this
- anyway most current installations don't have troubles with internet
access what was main motivation for this configuration directive
It has no effect anyway and in case we would want to make syntax
highlighting optional, it needs to be done in javascript and needs
better configuration name than this one.
