• Sylvain Dailler's avatar
    fix #292 · 95dc27a6
    Sylvain Dailler authored
    Add an option in the preferences to disallow the automatic jump after a
    goal is completed. Jump can still be performed by calling next in command
    line.
    95dc27a6
gconfig.ml 46.8 KB