#!/bin/sh
-# $Id: make_sed.sh,v 1.17 2023/06/25 18:13:17 tom Exp $
+# $Id: make_sed.sh,v 1.18 2023/11/25 14:31:18 tom Exp $
##############################################################################
# Copyright 2020-2022,2023 Thomas E. Dickey #
# Copyright 1998-2005,2017 Free Software Foundation, Inc. #
-e 's/$/\//' >$UPPER
{
+echo "# This script was generated from '$1' by man/make_sed.sh."
echo "# Do the TH lines"
sed -e 's/\//\/TH /' \
-e 's/ / /' \