rename "push" to "webPush" for future-proofing

This commit is contained in:
2023-12-02 15:28:32 -07:00
parent ee6a344daf
commit 3bf8fd0c22
4 changed files with 15 additions and 15 deletions

View File

@@ -20,7 +20,7 @@ export type Settings = {
lastViewedClaimId?: string; // Last viewed claim ID
lastNotifiedClaimId?: string; // Last notified claim ID
isRegistered?: boolean;
pushServer?: string; // Push server URL
webPushServer?: string; // Web Push server URL
// Array of named search boxes defined by bounding boxes
searchBoxes?: Array<{