Eliminate some unnecessary logic.

diff --git a/v7/dist/make-dist-files b/v7/dist/make-dist-files
index 7d62959d6c8716d9087fd0df35194eeedc72748d..c3d955a22f736df7d3556e2e1a0d6d65bca7a614 100755 (executable)
--- a/v7/dist/make-dist-files
+++ b/v7/dist/make-dist-files
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-# $Id: make-dist-files,v 1.11 2001/01/08 20:52:12 cph Exp $
+# $Id: make-dist-files,v 1.12 2001/02/23 05:19:03 cph Exp $
 #
 # Copyright (c) 2000-2001 Massachusetts Institute of Technology
 #
@@ -56,13 +56,9 @@ rm -rf ${BUILD_DIR}
     make install-html DESTDIR=${BUILD_DIR}
 )
 
-${MKINSTALLDIRS} ${AUXDIR}
-${INSTALL_DATA} /scheme/v7/src/etc/optiondb.scm ${AUXDIR}/.
-
 ${MKINSTALLDIRS} ${AUXDIR}/doc
 ${INSTALL_DATA} /scheme/v7/src/COPYING ${AUXDIR}/doc/.
 
-${MKINSTALLDIRS} ${AUXDIR}/edwin/info
 ${INSTALL_DATA} /usr/local/info/dir ${AUXDIR}/edwin/info/.
 ${INSTALL_DATA} /usr/local/info/r4rs.* ${AUXDIR}/edwin/info/.
 ${INSTALL_DATA} /usr/local/info/r5rs.* ${AUXDIR}/edwin/info/.