Previous
Up
Next
Module
Gui_init
module
Gui_init:
sig
..
end
Very early initialization step required by any GUI. This interface should be empty.