diff options
Diffstat (limited to 'driver/Frontend.mli')
| -rw-r--r-- | driver/Frontend.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Frontend.mli b/driver/Frontend.mli index d0514d01..39f0e612 100644 --- a/driver/Frontend.mli +++ b/driver/Frontend.mli @@ -22,3 +22,6 @@ val prepro_actions: (Commandline.pattern * Commandline.action) list val prepro_help: string (** Commandline help description *) + +val init: unit -> unit + (** Initialize the Frontend *) |