Use "src/etc/optiondb.scm" for distribution, _not_ our hacked one.

diff --git a/v7/dist/make-dist-files b/v7/dist/make-dist-files
index b983706b2ff2ca7d61b70e6595da006b959ea88a..b0672b1e41327daf1990fc2c8f82c3ec9c8829ea 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.8 2000/12/23 05:52:22 cph Exp $
+# $Id: make-dist-files,v 1.9 2000/12/23 06:04:02 cph Exp $
 #
 # Copyright (c) 2000 Massachusetts Institute of Technology
 #
@@ -54,6 +54,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/.