--- a/src/mkgendoc	Mon Jan 13 15:10:39 2003 +0000
+++ b/src/mkgendoc	Thu Jan 16 20:15:15 2003 +0000
@@ -1,5 +1,7 @@
 #! /bin/sh
 
+SED=${SED:-'sed'}
+
 if test $# -ne 1; then
   echo "usage: mkgendoc f1" 1>&2
   exit 1
@@ -67,7 +69,7 @@
 EOF
 
 for file in $DOC_FILES; do
-  fcn=`echo $file | sed 's,^\./,,; s/\.df//; s/-/_/g'`
+  fcn=`echo $file | $SED 's,^\./,,; s/\.df//; s/-/_/g'`
   echo "static void"
   echo "print_${fcn}_doc_strings (void)"
   echo "{"
@@ -84,7 +86,7 @@
 EOF
 
 for file in $DOC_FILES; do
-  fcn=`echo $file | sed 's,^\./,,; s/\.df//; s/-/_/g'`
+  fcn=`echo $file | $SED 's,^\./,,; s/\.df//; s/-/_/g'`
   echo "  print_${fcn}_doc_strings ();"
 done