Maybe we should use the .php extension for all config files? Even
if>>they aren't PHP sourcefiles? This way their contents could be
protected by a line like this on top:
# <?php exit()?>
Good news: I have the patch, along the lines discussed earlier.
Bad news: it doesn't work :-)
It turns out that lines starting with '#' are *also*
comments in php (Grr!). So the php code has to be
uncommented - and we have to be careful with the
parsing of the files.
