Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

gconfig.mli 268 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17


type t = 
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
    }

val read_config : unit -> t

val save_config : t -> unit

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
End: 
*)