*** src/backend/catalog/genbki.sh.orig	Thu Jul  6 22:33:22 2000
--- src/backend/catalog/genbki.sh	Sun Jul  9 09:00:01 2000
***************
*** 45,57 ****
              INCLUDE_DIR="$2"
              shift;;
          -I*)
!             INCLUDE_DIR=`echo $1 | sed s/^-I//`
              ;;
          -o)
              OUTPUT_PREFIX="$2"
              shift;;
          -o*)
!             OUTPUT_PREFIX=`echo $1 | sed s/^-o//`
              ;;
          --help)
              echo "$CMDNAME generates system catalog bootstrapping files."
--- 45,57 ----
              INCLUDE_DIR="$2"
              shift;;
          -I*)
!             INCLUDE_DIR=`echo $1 | sed -e 's/^-I//'`
              ;;
          -o)
              OUTPUT_PREFIX="$2"
              shift;;
          -o*)
!             OUTPUT_PREFIX=`echo $1 | sed -e 's/^-o//'`
              ;;
          --help)
              echo "$CMDNAME generates system catalog bootstrapping files."