libtock-rs icon indicating copy to clipboard operation
libtock-rs copied to clipboard

Rename `driver_number` to `driver_num`

Open jrvanwhy opened this issue 3 years ago • 2 comments

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.

jrvanwhy avatar Feb 08 '22 19:02 jrvanwhy

I think #373 solves this.

alexandruradovici avatar Feb 18 '22 13:02 alexandruradovici

I think #373 solves this.

#373 replaced DRIVER_ID with DRIVER_NUM, but there's still a mix of DRIVER_NUM and DRIVER_NUMBER.

jrvanwhy avatar Feb 18 '22 16:02 jrvanwhy

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

bradjc avatar Aug 08 '23 22:08 bradjc

Looks finished to me too.

jrvanwhy avatar Aug 08 '23 22:08 jrvanwhy