Skip to content

Commit

Permalink
MeetingGrid: instead of erroring on unknown users or times, just drop…
Browse files Browse the repository at this point in the history
… them silently
  • Loading branch information
achlipala committed Feb 10, 2015
1 parent 465cd4a commit 41d36d0
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions meetingGrid.ur
Original file line number Diff line number Diff line change
Expand Up @@ -621,13 +621,13 @@ functor Make(M : sig
let
fun tweakUses uses =
case uses of
[] => error <xml>FullGrid.tweakMeeting: unknown us</xml>
[] => return ()
| (us', _, tms) :: uses' =>
if us' = us then
let
fun addTimes tms =
case tms of
[] => error <xml>FullGrid.tweakMeeting: unknown time</xml>
[] => return ()
| (tm', _, ths) :: tms' =>
if tm' = tm then
v <- get ths;
Expand Down Expand Up @@ -757,7 +757,7 @@ functor Make(M : sig
let
fun addTimes tms =
case tms of
[] => error <xml>One.tweakMeeting: unknown time</xml>
[] => return ()
| (tm', ths) :: tms' =>
if tm' = tm then
v <- get ths;
Expand Down

0 comments on commit 41d36d0

Please sign in to comment.