Closes #126

mirabilos authored 5 years ago and mirabilos committed 5 years ago

While, strictly speaking, the file basename (without extension)
does not matter, supply one, as the wildcard keeps tripping up
contributors. Use the new name but (still) the older directory
until the code looks in the new directory.

mirabilos authored 5 years ago and mirabilos committed 5 years ago

(everywhere but in LICENCE which has a separate fixup branch;
keep docs/make.bat in CR-LF line endings)