diff options
Diffstat (limited to 'Build/source/texk/detex/detex-src/detex.l')
-rw-r--r-- | Build/source/texk/detex/detex-src/detex.l | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Build/source/texk/detex/detex-src/detex.l b/Build/source/texk/detex/detex-src/detex.l index 02f6db80546..0b0590a97ff 100644 --- a/Build/source/texk/detex/detex-src/detex.l +++ b/Build/source/texk/detex/detex-src/detex.l @@ -423,6 +423,7 @@ VERBSYMBOL =|\\leq|\\geq|\\in|>|<|\\subseteq|\subseteq|\\subset|\\supset|\\sim|\ /* escaping commands */ <Normal>"\\slash" putchar('/'); +<Normal>"\\%" putchar('%'); <Normal>\\(aa|AA|ae|AE|oe|OE|ss)[ \t]*[ \t\n}] /* handle ligatures */ {(void)printf("%.2s", yytext+1);} <Normal>\\[OoijLl][ \t]*[ \t\n}] {(void)printf("%.1s", yytext+1);} |