Use an alternative style for the diffs
commit8c457e9f83a0715cbaad395365f856cdc2f605f9
authorPieter de Bie <pdebie@ai.rug.nl>
Sun, 28 Sep 2008 18:48:55 +0000 (28 20:48 +0200)
committerPieter de Bie <pdebie@ai.rug.nl>
Sun, 28 Sep 2008 18:48:55 +0000 (28 20:48 +0200)
tree1c1cf8d0b1a67cd814a69544f341dc54fea09258
parent8835624d29380e7843e1ae94974a096593da1d37
Use an alternative style for the diffs
html/diffHighlighter.js
html/diff_style.css