Which software emits dates in this format between dollar signs when exporting?

Sometimes I see dates enclosed in between two $ (dollar) signs, eg. $Date: 2018/11/11 10:05:10 $ or $Date: Tuesday 06 April 2004 - 14:10:05$. I've seen this mostly on personal homepages, most probably written in some markup language and then exported to HTML, and once in a PDF document. The HTML source code did not have any relevant meta tag (such as generator) and websearch is not very good when it comes to special characters, so... My question is which software produces this output.