tree 8a5f7e36c34f4c4b0339fc6b46acf6b1f6d06e87
parent 0f4aea24d9c841ed6c62320a10ec59075ed9c94c
author Christopher Guindon <chris.guindon@eclipse.org> 1371737356 -0400
committer Christopher Guindon <chris.guindon@eclipse.org> 1371737356 -0400

lower font-size by 1px for highlights.