diff options
| author | Alban Gruin | 2021-10-04 12:46:08 +0200 |
|---|---|---|
| committer | Alban Gruin | 2021-10-04 12:46:08 +0200 |
| commit | 3bed39113f475ae9b1243ab6a018169ef9bf8c92 (patch) | |
| tree | b94824807833d66f6ec37ea2665268a8e97560d6 /src/course.ml | |
| parent | cee4a3ef6aba480b54ae32b427ce4579832e5d69 (diff) | |
course, ics: location may be empty, make it an option
As there may not be a location, make it an option type so we can easily
add a warning in the title of an event.
Signed-off-by: Alban Gruin <alban at pa1ch dot fr>
Diffstat (limited to 'src/course.ml')
| -rw-r--r-- | src/course.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/course.ml b/src/course.ml index 5ce2564..566ee0d 100644 --- a/src/course.ml +++ b/src/course.ml @@ -57,8 +57,8 @@ let loc_and_sum_to_groups = function | Groups groups | Summary (groups, _) | Location (groups, _, _) -> groups let loc_and_sum_to_location = function - | Nothing | Groups _ | Summary _ -> "" - | Location (_, _, location) -> location + | Nothing | Groups _ | Summary _ -> None + | Location (_, _, location) -> Some location let loc_and_sum_to_summary category = function | Nothing | Groups _ -> category |