# HG changeset patch # User wenzelm # Date 1605628098 -3600 # Node ID 2a329baa7d397b6cb8cc0a8f7ab456b1181dd736 # Parent 5cea0993ee4fbb8553cb009a7d28267e4692d264 proper link location; diff -r 5cea0993ee4f -r 2a329baa7d39 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Nov 17 16:34:01 2020 +0100 +++ b/src/Pure/Thy/present.ML Tue Nov 17 16:48:18 2020 +0100 @@ -42,9 +42,9 @@ val link = html_name thy'; in if session = session' then SOME link - else if chapter = chapter' then SOME (Path.parent + Path.basic session + link) - else if chapter = Context.PureN then NONE - else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) + else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link) + else if chapter' = Context.PureN then NONE + else SOME (Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link) end; fun theory_document symbols A Bs body =