Commit d15355a1 authored by André Anjos's avatar André Anjos 💬

Merge branch 'bob-devtools' into 'master'

Port package to new bob.devtools-based build system (c.f. bob/docs#7)

See merge request !10
parents 88b4e351 49789d13
Pipeline #31579 passed with stages
in 6 minutes and 51 seconds