diff make-dist @ 4203:b42338a458a5

(Man-set-fonts): Don't look for another char after the backspace; instead look for a sequence CHAR BS CHAR BS CHAR BS... Delete all the CHAR BS pairs found, after making the text property.
author Richard M. Stallman <rms@gnu.org>
date Wed, 21 Jul 1993 09:05:18 +0000
parents c720be6f3fae
children 15c60018d647
line wrap: on
line diff