faster strip_files() function

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.