aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
authormarche2004-04-06 14:53:46 +0000
committermarche2004-04-06 14:53:46 +0000
commitbb9a7e78191df7df4a7d6af6459232fb31bd1b59 (patch)
tree3a790e3688a912668b360cc68d2523c5eacc31d3 /contrib/xml
parent41d6548d171317a54ee220afa67a5b0b13f7e00b (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')
0 files changed, 0 insertions, 0 deletions