From 739ead8b2d70f978e31f793234d7a633636742a1 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 13 May 2016 17:57:06 -0400
Subject: -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
```
---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 59015742e7..24f4b2a775 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1272,7 +1272,7 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro
 {\tt stop profiling}.
 \end{quote}
 
-You can also pass the {\tt -profileltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end.
+You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end.
 
 Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
 
-- 
cgit v1.2.3