diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 00:43:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 00:43:03 +0000 |
| commit | cfed30e1257a7d18a7e8675d7d099bf469ccb1ce (patch) | |
| tree | 2780f6aea1d9d9ba7885f8fa5999a1c28fbda4ff /Makefile.devel | |
| parent | 780d48143f5d91f3074ba1334d6b6cc8ab852c02 (diff) | |
Make value of pg-special-char-regexp depend on proof-shell-unicode.
This makes sure that stripping special characters from output is accurate.
Diffstat (limited to 'Makefile.devel')
0 files changed, 0 insertions, 0 deletions