~title:"A .moo can be generated"
~message:(Printf.sprintf
"%s can be generated for %s.\n<i>Should I generate it?</i>"
- mooname fname)
+ (Filename.basename mooname) (Filename.basename fname))
~parent ()
in
let b =
~default:BuildTimeConf.default_font_size "matita.font_size"
in
let source_buffer = source_view#source_buffer in
-(* let _ =
- source_view#event#connect#selection_clear (fun _ ->
- prerr_endline "source_view: selection clear";
- false)
- in *)
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
(*~comments:"comments"*)
~copyright:"Copyright (C) 2005, the HELM team"
~license:(String.concat "\n" (parse_txt_file "LICENSE"))
- (*?logo:GdkPixbuf.pixbuf*)
- (*?logo_icon_name:string*)
+ ~logo:
+ (GdkPixbuf.from_file
+ (BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png"))
~name:"Matita"
~version:BuildTimeConf.version
~website:"http://helm.cs.unibo.it"