tree 4503ffc10e13f2c532a47a40338db3b75e551936
parent 5d75fd9473f330e71eca5477e496aa240873314f
author Davide Pesavento <davide.pesavento@lip6.fr> 1502340368 -0400
committer Davide Pesavento <davide.pesavento@lip6.fr> 1502342411 -0400

ci: preserve PATH when running waf under sudo

Change-Id: Id178dba19d34b8f5f76de34cfe8407078e2f3409
Refs: #4186