#!/bin/sh
sed -e 's/{\\ptt[ ]*\\char[ ]*'
"'"
'137}/_/g' <
"
$1
"
>
"@
$1
"
&& mv
"@
$1
"
$1
syntax highlighted by
Code2HTML
, v. 0.9.1