doc: rename some html assets
authorRamprasad Venkataraman <ramv@illinois.edu>
Tue, 7 Aug 2012 15:56:09 +0000 (10:56 -0500)
committerRamprasad Venkataraman <ramv@illinois.edu>
Tue, 7 Aug 2012 15:56:09 +0000 (10:56 -0500)
commit46a2d69a6f6fb5027246e56764cd6ab75c63d09b
tree83380ece5d1b62b4ad7839893181bb97e3900fb0
parentd909c0b5e08748f890eff6ad60cdc9c0e986368b
doc: rename some html assets
doc/assets/hatchbkgd.png [moved from doc/assets/navbarbkgd.png with 100% similarity]
doc/assets/head.html
doc/assets/manual.css
doc/assets/manual.js [moved from doc/assets/hilitesyntax.js with 100% similarity]