ros-infrastructure/jenkins_scripts — pull request #72 by dirk-thomas (2014-06-06 19:03:21+00:00)
Title: only install package not yet installed

This way it is possible to run the `devel` script with the `--no-chroot` option without requiring `sudo` - at least if all dependencies are already there.

@tfoote Please review.