diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 39a12a7ea7..871a7f15cb 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -214,7 +214,6 @@ let theory_filename xml_library_root = None -> None (* stdout *) | Some xml_library_root' -> let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in - let hd = List.hd toks in (* theory from A/B/C/F.v goes into A/B/C/F.theory *) let alltoks = List.rev toks in Some (join_dirs xml_library_root' alltoks ^ ".theory") |