20 Jul
2017
20 Jul
'17
3:15 p.m.
On Friday, 14 July 2017 15:39:31 CEST Richard W.M. Jones wrote:
+let md_detail md = + let out = command "mdadm" ["-D"; "--export"; md] in + + (* Split the command output into lines. *) + let out = String.trim out in + let lines = String.nsplit "\n" out in
If here we do: let lines = List.filter ((<>) "") lines in then later on we can use List.map instead of filter_map. -- Pino Toscano