diff options
| -rw-r--r-- | etc/pagemenu.html | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/etc/pagemenu.html b/etc/pagemenu.html index 2bb9d1c06..67601b655 100644 --- a/etc/pagemenu.html +++ b/etc/pagemenu.html @@ -13,7 +13,9 @@ {%- if show_source and has_source and sourcename %} <li><a href="{{ pathto('_sources/' + sourcename, true)|e }}" rel="nofollow">{{ _('Show Source') }}</a></li> + {%- else %} + {# Note: single HTML won't have source rst #} + <li><a href="//pdfcrowd.com/url_to_pdf/">Save to PDF</a></li> {%- endif %} - <li><a href="//pdfcrowd.com/url_to_pdf/">Save to PDF</a></li> </ul> </div> |