var files_dup =
[
    [ "kernel", "dir_dc43877d82dd332f9fb2071fcca799d6.html", "dir_dc43877d82dd332f9fb2071fcca799d6" ]
];