From 64b6b6075e461383719f6565aff2976dacc47569 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Thu, 17 Aug 2017 14:56:46 -0400 Subject: use OCaml temp_file, instead of our own version --- doc/refman/RefMan-tac.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ba9b21bfd..6e2735700 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3326,9 +3326,9 @@ evaluating purely computational expressions (i.e. with little dead code). \begin{quote} {\tt Set NativeCompute Profile Filename \str} \end{quote} - to specify the profile output; the default is {\tt native\_compute\_profile.data}. If there's an existing file with - the specified name, \Coq{} will append a number to it to avoid name collisions. That means you can - individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on + to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used + will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means + you can individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on the profile file to see the results. Consult the {\tt perf} documentation for more details. \end{Variants} -- cgit v1.2.3