<?php
/*
 * The 404-handler is very tightly tied to the default theme,
 * such that it would be easier to write a new handler for a
 * new theme than to alter this one...
 */
?>