Use the Unicode divisor sign.

2026-09-10 07:16:29 -04:00 · 2020-07-18 05:15:44 +02:00 · 2020-07-18 05:15:44 +02:00 · 75c61edf53
parent bdf3d48c5e
commit 75c61edf53
1 changed files with 1 additions and 1 deletions
--- a/2
+++ b/2
@ -109,7 +109,7 @@
                    (idx2 = $on_demand_skip[(I)$p])
                )) {
                    idx2=$on_demand_skip[(I)$p]
-                    local idtxt="{dbg}$p "
+                    local idtxt="{dbg}${p//\//∕} "
                    if (( idx1 && !idx2 )) {
                        skipped+=( $REPLY )
                        idtxt+="{warn}a/l{rst}"