diff options
| author | gareuselesinge | 2013-05-16 14:28:31 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-05-16 14:28:31 +0000 |
| commit | 864bfe20e1e40b9c38d983aba65429bc940a3475 (patch) | |
| tree | 41db799c0641f00f1b3042c32d16ae94d76b8119 /plugins/syntax | |
| parent | c397bcc14c2d7ca527f2dd9d5cb8724880e7a2b6 (diff) | |
std_ppcmds is persistent, errors can be printed twice
The patch is very simple and naive, there is no lazy involved.
This makes a difference only for strbrk.
An extra patch may be necessary if there is a noticeable slowdown.
In any case the data type used is opaque, to ease any future optimization.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16528 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions