tree 744c85a451480d99700ac07e07936ee31449c83a
parent c7164827a951d924d07df7caae03096ea6b0d09a
author Andrew Yourtchenko <ayourtch@gmail.com> 1632817586 +0200
committer Damjan Marion <dmarion@me.com> 1632986613 +0000

misc: package the devtool plugins

a274c3a2ed8c4f1f38cb6f126326b4e6798869d2 has split the devtool plugins into a separate component,
which caused them not to be packaged as part of the existing .deb, however this can still be useful
to have them.

This commit adds the new deb vpp-plugin-devtools which contains that component.

Change-Id: I3cf44493745c3d4951ffd2194c6ae539e8ad5926
Type: fix
Signed-off-by: Andrew Yourtchenko <ayourtch@gmail.com>