faster strip_files() function
Tested with a port with 5500 output files, from which 53 candidates
for stripping. The timing was:
- 30 secs (old code)
- 0.2 secs (new code - current patch)
- 1.4 secs (new code with proper quoting - not commited)
Most of the time is spent in getting the output from the file program.
The old code started the file program for every file.
The new/present code starts N=$(nproc) processes in parallel with 10 input
files for each 'file' process. The output of the file program is feed
to an awk process which filters-out only the candidates for stripping.
This process runs in parallel too (but with one file per strip process).
The --no-buffer options is used because it sounds good (the strip should
start as soon as one of the file processes has a verdict for one of
their 10 files), but I didn't measure it.
The "xargs -r -L10 -P$N" command will miss the files with spaces.
For a file named "a b" it will spawn:
file "a" "b"
A slower version, with proper quoting, "xargs -r -L1 -P$N -I{} file ... '{}'",
will spawn:
file "a b"
* xargs will force -L1 if -I{} is used
Given that the file process doesn't return error codes for non-existing
files, and that there is a very low probability that we have ports with
filenames constaining spaces that are worth stripping them, I choose to
keep the faster (non perfect) version.