Rewrite read_lines and use List.filter_map
authorStéphane Glondu <glondu@debian.org>
Sun, 20 Aug 2023 09:09:06 +0000 (11:09 +0200)
committerStéphane Glondu <glondu@debian.org>
Sun, 20 Aug 2023 09:09:37 +0000 (11:09 +0200)
commite3c1f864a80914873a75aba7281e49cfbb4ac05d
tree3b0d2f60f1828641fa42e0a929544978fd9be714
parentb13043695ee78c73bf9ea5c4c0d1c96b7ef2b92c
Rewrite read_lines and use List.filter_map
debian/dispatch.ml