diff options
| author | glondu | 2010-12-03 19:06:22 +0000 |
|---|---|---|
| committer | glondu | 2010-12-03 19:06:22 +0000 |
| commit | 321969d18e24a6c636137efd0a59a254603fce94 (patch) | |
| tree | b4994d54360cabe6f6245ce9c2d114fb1f00b93e /plugins/syntax/string_syntax.ml | |
| parent | 0d87d99747d1ad6b8a69672b08a2bb5b2174adc6 (diff) | |
Redirect stdout to stderr in -ideslave
This fixes "Print Grammar" in coqide, which uses a camlp5 function
that prints to stdout, interfering with the ide-slave
communication. Camlp5 should additionnally provide a way to print to a
formatter instead of directly using stdout...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions