diff make-dist @ 18693:7113c3fe2d3a

Fix previous change.
author Richard M. Stallman <rms@gnu.org>
date Wed, 09 Jul 1997 04:49:35 +0000
parents 678528c8dd4f
children 4a53a2477850
line wrap: on
line diff
--- a/make-dist	Wed Jul 09 04:47:12 1997 +0000
+++ b/make-dist	Wed Jul 09 04:49:35 1997 +0000
@@ -159,11 +159,17 @@
 losers="`comm -23 /tmp/el /tmp/elc`"
 bogosities=
 for file in $losers; do
-  if ! grep -q "dontcompilefiles:.* $file\($\| \)" lisp/Makefile; then
-    if [ "$file" != site-init.el ] && [ "$file" != site-load.el ] \
-       && [ "$file" != site-start.el ] && [ "$file" != default.el ]; then
-      bogosities="$file $bogosities"
-    fi
+  file1=`echo $file | sed -e "s|.*/||"`
+  if ! grep -q "dontcompilefiles:.* $file1\($\| \)" lisp/Makefile; then
+    case $file in
+      site-init.el | site-load.el | site-start.el | default.el)
+        ;;
+      term/*)
+        ;;
+      *)
+        bogosities="$file $bogosities"
+	;;
+    esac
   fi
 done
 if [ x"${bogosities}" != x"" ]; then