diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-05-13 17:57:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:40 -0400 |
| commit | 739ead8b2d70f978e31f793234d7a633636742a1 (patch) | |
| tree | 15da3b48ea04a45333dbe6484f4f47badb912d35 /tools/coqc.ml | |
| parent | 51b32595081d279624c8ec162f9ed686ed660d9b (diff) | |
-profileltac -> -profile-ltac, as per @herbelin
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
Diffstat (limited to 'tools/coqc.ml')
| -rw-r--r-- | tools/coqc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index 7210efc4f..18b2a24fa 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -88,7 +88,7 @@ let parse_args () = (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profileltac" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |