diff options
Diffstat (limited to 'man/make_sed.sh')
| -rwxr-xr-x | man/make_sed.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/man/make_sed.sh b/man/make_sed.sh index f2afac93ebc8..55ba32f528c6 100755 --- a/man/make_sed.sh +++ b/man/make_sed.sh @@ -1,7 +1,7 @@ #!/bin/sh -# $Id: make_sed.sh,v 1.9 2005/07/16 18:15:31 tom Exp $ +# $Id: make_sed.sh,v 1.10 2017/08/12 12:22:06 tom Exp $ ############################################################################## -# Copyright (c) 1998-2003,2005 Free Software Foundation, Inc. # +# Copyright (c) 1998-2005,2017 Free Software Foundation, Inc. # # # # Permission is hereby granted, free of charge, to any person obtaining a # # copy of this software and associated documentation files (the "Software"), # @@ -45,7 +45,7 @@ UPPER=upper$$ SCRIPT=script$$ RESULT=result$$ rm -f $UPPER $SCRIPT $RESULT -trap "rm -f $COL.* $INPUT $UPPER $SCRIPT $RESULT" 0 1 2 5 15 +trap "rm -f $COL.* $INPUT $UPPER $SCRIPT $RESULT" 0 1 2 3 15 fgrep -v \# $1 | \ sed -e 's/[ ][ ]*/ /g' >$INPUT |