#!/usr/bin/awk -f
#Requires BSD awk (not gawk!).
/section/ {
        gsub("\\\\(sub)*section{","")
        gsub("}","")
        gsub("\\\\texttt{","")
        section = $0
}
/begin{code}/ {
        if (section != "") {
                print "==== " section " ===="
                section = ""
        }
        print "<code bash>"
}
 
/end{code}/ {
        print "<\/code>"
}
/begin{code}/, /end{code}/ {
        if ( $0 ~ /begin{code}/ || $0 ~ /end{code}/ ) {} else {
        gsub("\\\\_","_")
        gsub("\\\\\\$","$")
        gsub("\\\\&","\\&")
        gsub("\\\\{","{")
        gsub("\\\\}","}")
        gsub("\\\\#","#")
        gsub("\\\\%","%")
        gsub("\\\\\\^","^")
        gsub("\\\\textbackslash","\\")
        print
        }
}