From b118abe6e411f5e9ac6f7adc17de602bdf4a0830 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:24:44 +0000 Subject: [PATCH] added cmdline alias "command" for "tactica" --- helm/ocaml/cic_disambiguation/test_parser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index b7cace0cb..356c0a369 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -33,7 +33,7 @@ let mode = | "alias" -> prerr_endline "Alias"; `Alias | "term" -> prerr_endline "Term"; `Term | "tactic" -> prerr_endline "Tactic"; `Tactic - | "tactical" -> prerr_endline "Tactical"; `Tactical + | "tactical" | "command" -> prerr_endline "Tactical"; `Tactical | "script" -> prerr_endline "Script"; `Script | _ -> prerr_endline "What???????"; -- 2.39.2