From: Claudio Sacerdoti Coen Date: Fri, 14 Jan 2011 12:10:42 +0000 (+0000) Subject: Bug fixed: the script windows did not scroll correctly because I used the X-Git-Tag: make_still_working~2590 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=423c4e6702b28ae9b017078fb8fcbc7976956318;p=helm.git Bug fixed: the script windows did not scroll correctly because I used the wrong method. --- diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index fafd7cdb2..af3cdf12e 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -247,7 +247,7 @@ let source_view = ~insert_spaces_instead_of_tabs:true ~tab_width:2 ~right_margin_position:80 ~show_right_margin:true ~smart_home_end:`AFTER - ~packing:parent#add_with_viewport + ~packing:parent#add () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in