From 10fe193634df36df5f3047a7a74b910dd143cbb4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2001 16:44:28 +0000 Subject: [PATCH] Forward and backward metadata added to the Raw menu. OPEN BUG: asking metadata for inductive types does not work. A window requesting which metadata to show should be opened instead. --- helm/on-line/html/library/control.html | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html index 5d353fc0d..501e1d028 100644 --- a/helm/on-line/html/library/control.html +++ b/helm/on-line/html/library/control.html @@ -38,6 +38,8 @@ outputOption(document, "cic", "CIC", mode_list[1]); outputOption(document, "types", "TYPES", mode_list[1]); outputOption(document, "ann", "ANN", mode_list[1]); + outputOption(document, "fwd", "RDF: Forward pointers", mode_list[1]); + outputOption(document, "bwd", "RDF: Backward pointers", mode_list[1]); } else { outputOption(document, "html", "HTML", mode_list[2]); outputOption(document, "mml_cont", "MathML Content", mode_list[2]); -- 2.39.2