Make diffs more easily copy/pastable

[joukevandermaas]

Example of what happens now:

It would be great if the line numbers (and maybe even + and - symbols) did not get selected when selecting text in the diff. For an example, see Github diffs.

[sivakumar-kailasam]

@joukevandermaas tried user-select: none and learnt that webkit lets you copy text from an element that has user-select:none while firefox doesn't, so 😿

related webkit issue: https://bugs.webkit.org/show_bug.cgi?id=80159