diff options
| author | Alban Gruin | 2021-09-16 21:55:11 +0200 |
|---|---|---|
| committer | Alban Gruin | 2021-09-19 12:37:38 +0200 |
| commit | 9a84c508cd498c4331e35407f1da192fff8a6d19 (patch) | |
| tree | a221a1d72c804018660da1a616f3eb6cde197bdb /dune-project | |
| parent | cb2f075c326f40c27b4c6d9dde6fd51b78a43f9c (diff) | |
server: allow to fetch module timetables in addition to groups
This add a new type, fetch_kind, and a function, kind_to_res_type, to
select the type of timetable we want to fetch: Group, or Module. For
now, Module is not used, so warning 37 is disabled in fetch_kind. It
will be enabled back in the next commit.
Signed-off-by: Alban Gruin <alban at pa1ch dot fr>
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions