At first, I thought it is the same font as code (i.e.,
But the comparation(left: line number, right: code) above shows that they are not.
However, it is not a monospace font. When I applied it on the website, it shows:
I guess it is a variant of D-DIN font, but anybody knows what font exactly it is?