web: Don't duplicate the html header.
authorAndre Noll <maan@tuebingen.mpg.de>
Mon, 15 Jun 2020 23:39:18 +0000 (01:39 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Tue, 22 Sep 2020 19:28:31 +0000 (21:28 +0200)
commitf497ad60e2191188f6bef05d022a07d17c65a357
tree728cac628e35e916c6bfabde8ea8a36e073c2176
parent7a5132c93cde8ce79bbea3dc4568ffa5f42ec5cf
web: Don't duplicate the html header.

Now that all web pages are in a single directory, we can get rid of
some duplication by using header.html also to create index.html.
Makefile
web/index.html.in