diff options
| author | Jonas Berlin <xkr47@outerspace.dyndns.org> | 2020-02-17 22:59:37 +0200 |
|---|---|---|
| committer | Flavio Castelli <fcastelli@suse.com> | 2021-04-19 14:51:14 +0200 |
| commit | b3670ece0ec72610ad31283c6b6b2c7f556eeba1 (patch) | |
| tree | a5d64e93b9a7bced32f75e5421ea1a4fb9d042d1 /src/config.rs | |
| parent | 94f7578576b150edb8167b82ee36828e50530c12 (diff) | |
Add "Suggest an edit" link next to "Git repository"
Includes new configuration option `git-repository-edit-baseurl` for
supporting non-GitHub repository layouts.
Diffstat (limited to 'src/config.rs')
| -rw-r--r-- | src/config.rs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/config.rs b/src/config.rs index be7dae62..1191542b 100644 --- a/src/config.rs +++ b/src/config.rs @@ -522,6 +522,11 @@ pub struct HtmlConfig { /// /// [custom domain]: https://docs.github.com/en/github/working-with-github-pages/managing-a-custom-domain-for-your-github-pages-site pub cname: Option<String>, + /// Git repository file edit baseurl, below which e.g. src/SUMMARY.md can + /// be viewed/edited + /// Defaults to git_repository_url + `/blob/master` if `None` and + /// git_repository_url is not `None` - works for e.g. GitHub master branch + pub git_repository_edit_baseurl: Option<String>, /// This is used as a bit of a workaround for the `mdbook serve` command. /// Basically, because you set the websocket port from the command line, the /// `mdbook serve` command needs a way to let the HTML renderer know where |