diff as an available language for highlighting

[gr-im]

When writing a manual using odoc (and odoc_driver), I sometimes find it useful to build blocks of code incrementally. For this, the diff language (available in highlight.js) seems to be a good approach. So I think it would be good to add it to the list of languages ‘natively’ supported by the bundle of hightligh.js provided by default. Especially as passing specific flags to odoc seems to be a complicated task at the moment.

Thanks a lot!