Merge branch 'devel' of ssh://git.planet-lab.org/git/nodemanager into devel