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