From a5995a69f37919b25a2b6d6885daa0877a41c0b3 Mon Sep 17 00:00:00 2001 From: Anders Kaseorg Date: Fri, 24 May 2024 11:41:49 -0700 Subject: [PATCH] people: Fix get_custom_profile_data type. Signed-off-by: Anders Kaseorg --- web/src/people.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/web/src/people.ts b/web/src/people.ts index b5cbde347a..0f4ef5a40b 100644 --- a/web/src/people.ts +++ b/web/src/people.ts @@ -1716,7 +1716,10 @@ export function my_custom_profile_data(field_id: number): ProfileData | null | u return get_custom_profile_data(my_user_id, field_id); } -export function get_custom_profile_data(user_id: number, field_id: number): ProfileData | null { +export function get_custom_profile_data( + user_id: number, + field_id: number, +): ProfileData | null | undefined { const person = get_by_user_id(user_id); const profile_data = person.profile_data; if (profile_data === undefined) {