From d3ea9396705da521afa6276f2b1039bd84794059 Mon Sep 17 00:00:00 2001
From: Paul Eggert <eggert@cs.ucla.edu>
Date: Fri, 29 Aug 2025 09:14:52 -0700
Subject: [PROPOSED 1/8] =?UTF-8?q?Work=20around=20groff=20-Tutf8=20misfeat?=
 =?UTF-8?q?ure=20with=20=E2=80=98*=E2=80=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* workman.sh (ASTERISK_OPERATOR): New var.  Use it to fix groff output.
---
 workman.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/workman.sh b/workman.sh
index 91621b10..e914553d 100644
--- a/workman.sh
+++ b/workman.sh
@@ -17,7 +17,10 @@ done
 
 groff="groff -dAD=l -rHY=0 $manflags -mtty-char -man -ww -P-bcou"
 if ($groff) </dev/null >/dev/null 2>&1; then
-  $groff "$@"
+  # Repair groff 1.23 -Tutf8 misfeature: it renders "*" as U+2217.  Do not put
+  # the bad character directly in this file, to pacify "make character-set.ck".
+  ASTERISK_OPERATOR=`printf '\342\210\227\n'` # U+2217
+  $groff "$@" | sed "s/$ASTERISK_OPERATOR/*/g"
 elif (type mandoc && type col) >/dev/null 2>&1; then
   mandoc $manflags -man "$@" | col -bx
 elif (type nroff && type perl) >/dev/null 2>&1; then
-- 
2.48.1