Re: [w3c/clipboard-apis] Add 'starts with' to web custom format prefix. (PR #195) from snianu on 2023-10-20 (public-webapps-github@w3.org from October 2023)

From: snianu <notifications@github.com>
Date: Fri, 20 Oct 2023 15:52:14 -0700
To: w3c/clipboard-apis <clipboard-apis@noreply.github.com>
Cc: Subscribed <subscribed@noreply.github.com>
Message-ID: <w3c/clipboard-apis/pull/195/review/1690977585@github.com>

@snianu commented on this pull request.



> @@ -717,7 +719,7 @@ url: https://w3c.github.io/permissions/#permissions-task-source; type: dfn;
 
    1. Let |isCustom| be |false|.
 
-   1. If |type| has "web "("web" followed by U+0020 SPACE) prefix, then:
+   1. If |type| [=string/starts with=] "web "("web" followed by U+0020 SPACE) prefix, then:
    
     1. Remove "web " prefix and set the remaining string to |type|.

Done.

-- 
Reply to this email directly or view it on GitHub:
https://github.com/w3c/clipboard-apis/pull/195#discussion_r1367535816
You are receiving this because you are subscribed to this thread.

Message ID: <w3c/clipboard-apis/pull/195/review/1690977585@github.com>

Received on Friday, 20 October 2023 22:52:23 UTC