Previous
Up
Next
Module
Ed_prefs
(
.ml
)
module
Ed_prefs:
sig
..
end
The preferences box.
val
edit_preferences
:
unit -> unit
Make the user edit the preferences in a modal window.