diff options
| author | stuebinm | 2021-12-16 00:30:30 +0100 |
|---|---|---|
| committer | stuebinm | 2021-12-16 00:30:30 +0100 |
| commit | 988b8fd7fdba5eee0b100401351199af918bc9e0 (patch) | |
| tree | c085899c48ef675043fb0fa115dbb60fa1379969 /src | |
| parent | f74bb6eb321f9a22be5cbdb6c92ed74e09226b18 (diff) | |
made a partial function total
(shouldn't have been called anyways, but it's still nice not to have it
fail if it ever does get called with that case)
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions