K 10 svn:author V 4 bapt K 8 svn:date V 27 2015-10-21T09:44:50.981601Z K 7 svn:log V 133 Rename libdevctl into libdevdctl In recent head there is already a libdevctl so we need to avoid conflicts Sponsored by: Gandi.net END