Use "doc" instead of "documentation".

diff --git a/v7/dist/make-doc-files b/v7/dist/make-doc-files
index 9f2bead8f5eca893223021f92febd01429faa7ba..58b790a528827b04635b24f94f99c10801623e3e 100755 (executable)
--- a/v7/dist/make-doc-files
+++ b/v7/dist/make-doc-files
@@ -1,7 +1,7 @@
 #!/bin/sh
 
 prefix=`/scheme/v7/dist/release-prefix`
-tldir=${prefix}/documentation
+tldir=${prefix}/doc
 mkdir ${prefix}
 mkdir ${tldir}