d72b4a3c1e
If two targets using the same OS are built in parallel, they can both try to install the same include/os/* file at the same time, causing the installEpics.pl script to die. We fix this by making all installations atomic: First copy the file to the installation directory using a unique name, then rename it to the target name. The target name is in the same directory and filesystem as the temporary name, so the rename should be atomic.