-
Committer:
Hugo Herbelin
-
Author(s):
notin
-
Date:
2016-03-08 09:47:25 UTC
-
Revision ID:
git-v1:6aecb9a1fe3f9b027dfd702931298bc61d40b6d3
Default CoqIDE modifiers for menu did not work (e.g. "d" was
activating the "d" template menu).
I backported svn revision 9349 from JMN which fixes the problem (even
though I don't know why the previous setting would have worked at some
early time around 2004, in 8.0, before 8.1 is released).
Log of r9349 was:
Changement des modifeurs par défaut dans CoqIDE (problème de
compatibilité entre architecture)