diff options
| author | courtieu | 2006-04-27 16:00:49 +0000 |
|---|---|---|
| committer | courtieu | 2006-04-27 16:00:49 +0000 |
| commit | c9f997fd32e3bccf58b9d3c26e1822a765c44d21 (patch) | |
| tree | c11c7e41d8a23fdffd0d6dcad2f963b77e59bde5 /dev/include | |
| parent | f8681aaa2f963f4a899dd208e5a6b86883d0dc5b (diff) | |
Modification of emacs output: Pp.warning and al now output warning
between special characters.
I had to add a hidden variable print_emacs and a function to set it to
true in Pp because using Options.print_emacs would have introduce a
circularity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions