From 1b1bde486d535fe9d211b1c82d05ec6e4b5fe80a Mon Sep 17 00:00:00 2001 From: Greg Lueck Date: Tue, 25 Jun 2024 17:59:24 -0400 Subject: [PATCH] Device selector might be called more than once The description of device selectors in the "Device selection" section does not say that a selector is called exactly once for each root device. Change the wording of the `platform` selector constructor to be consistent with this wording, leaving the number of times it is called ambiguous. We might want to reconsider this, though. Why wouldn't we want to require the selector to be called exactly once? --- adoc/chapters/programming_interface.adoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/adoc/chapters/programming_interface.adoc b/adoc/chapters/programming_interface.adoc index a7075ece..2bdae493 100644 --- a/adoc/chapters/programming_interface.adoc +++ b/adoc/chapters/programming_interface.adoc @@ -1001,8 +1001,8 @@ explicit platform(const DeviceSelector& selector) _Constraints:_ The [code]#DeviceSelector# must be a type that satisfies the requirements of a <> as defined in <>. -_Effects:_ The [code]#selector# is called once for every <> as -described in <>. +_Effects:_ The [code]#selector# is called for every <> as described +in <>. Constructs a [code]#platform# object that is a copy of the platform which contains the device that is selected by [code]#selector#.