path: root/html/develdownload

<?php include('develdownload.php'); ?>
<?php 
  /* This file needs some extra characters in it for apache to work its magic.
     Things work fine as link to index.html, but it's tricky to include links 
     in cvs. */ ?>