followup #15642: make source + edit also work with stdlib (which uses -d:boot) (#15684)

This commit is contained in:
Timothee Cour 2020-10-22 12:02:18 -07:00 • committed by GitHub
commit 2cb484cefb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -146,6 +146,7 @@ doc.body_toc_group = """
$body_toc_groupsection $body_toc_groupsection
$tableofcontents $tableofcontents
</div> </div>
$seeSrc
<div class="nine columns" id="content"> <div class="nine columns" id="content">
<div id="tocRoot"></div> <div id="tocRoot"></div>
$deprecationMsg $deprecationMsg
@ -156,7 +157,7 @@ doc.body_toc_group = """
""" """
@else @else
# keep in sink with other `doc.body_toc_group` or better, refactor
doc.body_toc_group = """ doc.body_toc_group = """
<div class="row"> <div class="row">
<div class="three columns"> <div class="three columns">