PR #1495 Use a common source of current device.

Use a common source of current device. #1495

dlibenzi merged 1 commit into master from common_current_device

dlibenzi requested a review from

mruberry 6 years ago

Use a common source of current device.

c1d55e70

dlibenzi force pushed from de44b510 to c1d55e70 6 years ago

mruberry approved these changes on 2019-12-20

dlibenzi merged b29de375 into master 6 years ago

dlibenzi deleted the common_current_device branch 6 years ago

Reviewers

mruberry

Assignees

No one assigned

Labels

None yet

Milestone

No milestone