Commit d18e01352c549452f924d8d942d131b6bd29b3ce

Werner Lemberg 2003-07-25T22:21:57

(code_header, code_footer): Don't change font colour directly but use a special <pre> class.