added to the CD-ROM (only if they exist), as proposed on tech-install
and tech-toolchain without objections. Note, this will "bloat" the CD-ROM
image if you have done a "./build.sh sourcesets". If you don't want that,
just move "source" out of ${RELEASEDIR} for the "make iso-image".
ca38156730