diff make-dist @ 108216:2fb32340c261

* make-dist: There are no more src/m/*.inp files.
author Glenn Morris <rgm@gnu.org>
date Sun, 02 May 2010 18:53:58 -0700
parents 1d1d5d9bd884
children 7303923cef22
line wrap: on
line diff
--- a/make-dist	Sun May 02 20:41:45 2010 -0400
+++ b/make-dist	Sun May 02 18:53:58 2010 -0700
@@ -469,8 +469,7 @@
 
 echo "Making links to \`src/m'"
 (cd src/m
- # We call files for miscellaneous input (to linker etc) .inp.
- ln README [a-zA-Z0-9]*.h *.inp ../../${tempdir}/src/m)
+ ln README [a-zA-Z0-9]*.h ../../${tempdir}/src/m)
 
 echo "Making links to \`src/s'"
 (cd src/s