Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 6aecb9a1 authored by Jean-Marc Notin's avatar Jean-Marc Notin Committed by HERBELIN Hugo
Browse files

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)
parent a4718efc
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment