# HG changeset patch
# User wenzelm
# Date 981210117 -3600
# Node ID 5873a05b4d21f2ba1b8e51d73a440bdf48497de7
# Parent  2e3bbac8763bf848ccac481721e2b628c46c2939
use fgrep;

diff -r 2e3bbac8763b -r 5873a05b4d21 bin/isatool
--- a/bin/isatool	Sat Feb 03 15:20:55 2001 +0100
+++ b/bin/isatool	Sat Feb 03 15:21:57 2001 +0100
@@ -38,7 +38,7 @@
       for T in *
       do
         if [ -f "$T" -a -x "$T" ]; then
-          DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
+          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
           echo "    $T - $DESCRLINE"
         fi
       done