Open Vampire opened 6 years ago
OS, IDE version?
Windows 10 IntelliJ IDEA 2018.1.5 Ultimate
I just found out that here Ctrl+Alt+Enter triggers the reload action (Ctrl+Enter just does apply like simple Enter).
works fine for me on Win 10 - without ctrl
If I am in the expression textfield of a grep console and press Alt+Enter like mentioned in the tooltip of the "Reload" button, nothing happens, not even the tab title is changed.