Skip to content
Snippets Groups Projects
Commit 637d4c08 authored by Bryan O'Sullivan's avatar Bryan O'Sullivan
Browse files

profile: expand PID in output file name

parent 3f9ce63d
No related branches found
No related tags found
No related merge requests found
...@@ -412,7 +412,10 @@ ...@@ -412,7 +412,10 @@
"hotshot" is deprecated, and produces less reliable results. "hotshot" is deprecated, and produces less reliable results.
Default is no profiling. Default is no profiling.
output;; output;;
The name of a file to write profiling data to. Default is stderr. The name of a file to write profiling data to. Each occurrence of
"%%p" will be replaced with the current process ID (the repeated
"%" protects against the config parser's string interpolator).
Default output is to stderr.
server:: server::
Controls generic server settings. Controls generic server settings.
......
...@@ -379,7 +379,8 @@ ...@@ -379,7 +379,8 @@
def profile_fp(): def profile_fp():
outfile = ui.config('profile', 'output', untrusted=True) outfile = ui.config('profile', 'output', untrusted=True)
if outfile: if outfile:
return open(outfile, 'w') pid = str(os.getpid())
return open(outfile.replace('%p', pid), 'w')
else: else:
return sys.stderr return sys.stderr
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment