aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Frontend.mli')
-rw-r--r--driver/Frontend.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Frontend.mli b/driver/Frontend.mli
index 39f0e612..a18c2704 100644
--- a/driver/Frontend.mli
+++ b/driver/Frontend.mli
@@ -18,7 +18,7 @@ val parse_c_file: string -> string -> Csyntax.coq_function Ctypes.program
(** From preprocessed C to Csyntax *)
val prepro_actions: (Commandline.pattern * Commandline.action) list
- (** Commandline optins affecting the frontend *)
+ (** Commandline options affecting the frontend *)
val prepro_help: string
(** Commandline help description *)