libtock-rs
libtock-rs copied to clipboard
Rename `driver_number` to `driver_num`
In https://github.com/tock/libtock-rs/pull/373, we noticed that this repository is split between using driver_number
/DRIVER_NUMBER
and driver_num
/DRIVER_NUM
. We decided to prefer driver_num
/DRIVER_NUM
for consistency with the main Tock repository.
We should replace all instances of driver_number
/DRIVER_NUMBER
in this repository with driver_num
/DRIVER_NUM
.
I think #373 solves this.
I think #373 solves this.
#373 replaced DRIVER_ID
with DRIVER_NUM
, but there's still a mix of DRIVER_NUM
and DRIVER_NUMBER
.
Looks finished?
$ cd git/libtock-rs
$ git grep driver_number | cat
unittest/src/fake/syscalls/allow_ro_impl_tests.rs:fn too_large_driver_number() {
unittest/src/fake/syscalls/allow_rw_impl_tests.rs:fn too_large_driver_number() {
$ git grep DRIVER_NUMBER | wc -l
0
Looks finished to me too.