ca38156730
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".