diff options
| author | marche | 2004-04-06 14:53:46 +0000 |
|---|---|---|
| committer | marche | 2004-04-06 14:53:46 +0000 |
| commit | bb9a7e78191df7df4a7d6af6459232fb31bd1b59 (patch) | |
| tree | 3a790e3688a912668b360cc68d2523c5eacc31d3 /contrib/xml/xmlcommand.ml | |
| parent | 41d6548d171317a54ee220afa67a5b0b13f7e00b (diff) | |
warning dialog when save fails
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5641 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions