diff options
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 7a8571fdcf..ab91537054 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -339,9 +339,13 @@ let print_leaf_entry with_values sep (sp,lobj) = [< >] | (_,"END-SECTION") -> [< >] | (_,"STRUCTURE") -> [< >] +(* To deal with forgotten cases... *) + | (_,s) -> [< >] +(* | (_,s) -> [< 'sTR(string_of_path sp); 'sTR" : "; 'sTR"Unrecognized object "; 'sTR s; 'fNL >] +*) let rec print_library_entry with_values ent = let sep = if with_values then " = " else " : " in |