Random Things

I had to rename many .phtml files, so that their extension will change to .php. This does the trick:


           for i in *.phtml; do mv $i ${i%.phtml}.php; done


This seems to work: (from the command line. php cli needs to be installed)

   echo "<?php echo highlight_file('file.php'); ?>" | php -q > file.html


Upload the resulting file and link it to the post as appropriate.

I often need to format reports such as phonebooks. It’s hard to get any better than TeX, so I like to combine them More… »