diff options
| author | vgross | 2009-12-07 16:55:21 +0000 |
|---|---|---|
| committer | vgross | 2009-12-07 16:55:21 +0000 |
| commit | 2f0e6e0a89babb9c4ee4e513d6cbd6de2f858a3a (patch) | |
| tree | 10d4ccf233a234660074c798cedaac355b2f8312 /ide | |
| parent | 8f4d0165f0a1be1b81ecab0356f7040423406c28 (diff) | |
Fix bug #2197 (option show_toolbar not taken into account at startup)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12568 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 99b2593087..fe71784b32 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3436,6 +3436,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); activate_input index; end; initial_about session_notebook#current_term.proof_view#buffer; + !show_toolbar !current.show_toolbar; session_notebook#current_term.script#misc#grab_focus () ;; |