diff options
| author | 2016-10-03 13:38:27 -0700 | |
|---|---|---|
| committer | 2016-10-03 15:33:06 -0700 | |
| commit | a5471a6723f4069f9c6e8d482d5a9045e58b695e (patch) | |
| tree | 20bc210b53471f2d278c4584a7cbfba710d93e08 /tools/fileslist_util.py | |
| parent | 647d38378806783510cb31cf9c2206cf9c3ec1c9 (diff) | |
exec makeparallel
bash doesn't kill children when it receives SIGTERM. Since makeparallel
is the last command run by the shell, run it with exec to replace the
shell with makeparallel so make can send the signal directly to
makeparallel.
Bug: 31907490
Test: m -j & killall make; pgrep -a makeparallel
Change-Id: If8aeb51ec224234da5f05eae3382ce77f48a57e2
Diffstat (limited to 'tools/fileslist_util.py')
0 files changed, 0 insertions, 0 deletions