[Git][monnier/typer][simon--pp-print] Change --indices to -Vindices to match other flags.
Simon Génier pushed to branch simon--pp-print at Stefan / Typer Commits: 7b1d8af8 by Simon Génier at 2023-02-27T16:19:36-05:00 Change --indices to -Vindices to match other flags. - - - - - 1 changed file: - typer.ml Changes: ===================================== typer.ml ===================================== @@ -135,7 +135,7 @@ let dump_tokens_main argv = let print_indices = ref false let dump_lexps_arg_defs = [ - ("--indices", + ("-Vindices", Arg.Set print_indices, "Print Debruijn indices in addition to variable names."); ] View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7b1d8af8c815452059713f83ceb98f512e... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/7b1d8af8c815452059713f83ceb98f512e... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Simon Génier (@ilovemonoids)