diff options
Diffstat (limited to 'contrib/xml/cic2acic.ml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 68514a6bea..e8718430d0 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -106,8 +106,6 @@ let token_list_of_kernel_name ~keep_sections kn tag = token_list_of_modpath path @ [N.string_of_label label] | N.MPfile dirpath -> token_list_of_dirpath dirpath | N.MPself self -> -(*CSC: ask Hugo if there is a better way *) -(*CSC: also check if multiple ways have been used *) if self = Names.initial_msid then [ "Top" ] else |
