chiark / gitweb /
Remove the redundant file headers.
authorMark Wooding <mdw@distorted.org.uk>
Sun, 6 Sep 2020 14:28:21 +0000 (15:28 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Mon, 7 Sep 2020 16:36:44 +0000 (17:36 +0100)
commitaecccf6c3d3688b8a30953b7fddc6e72d73b9465
tree83e116e50b037cf39b4e94237daec2c17cd85419
parent8995c091cfd0da790f531b32247cd1bab26258c2
Remove the redundant file headers.

Everything is duplicated in the GPL header anyway, and I can't get rid
of that.
19 files changed:
at.dtx
centre.dtx
cmtt.dtx
colour.dtx
crypto.dtx
doafter.dtx
exercise.dtx
footnote.dtx
mdwkey.dtx
mdwlist.dtx
mdwmath.dtx
mdwref.dtx
mdwtab.dtx
mdwthm.dtx
mdwtools.tex
poetry.dtx
slowbox.dtx
sverb.dtx
syntax.dtx