Thomas Lange Tue, 16 Jul 2019 17:46:18 -0700
we decided to remove /devel/people. See also 657647 and 727738
-- regards Thomas
