diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-11 10:35:47 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-11 10:35:47 +0100 |
| commit | b9585af9ef6e280ec1aa53e50833a3fa58c1763c (patch) | |
| tree | 74d1ba00dd59ded7e76b389d42c17735b1508e5f /doc/refman/RefMan-tac.tex | |
| parent | 4832692db5c21c178ff5825fc75496543f02875a (diff) | |
Fix CoqIDE compilation under standard version of lablgtk2
We use the win32 specific function only if WIN32 is defined
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
0 files changed, 0 insertions, 0 deletions