the "edit on github" button in doc fails

[tlienart]

https://alan-turing-institute.github.io/PDMP.jl/latest/

top right edit on Github -> 404. It seems to look for an index.md in docs/ however it's in docs/src as in Documenter.jl (https://github.com/JuliaDocs/Documenter.jl/tree/master/docs)

this is the irritating link: https://github.com/alan-turing-institute/PDMP.jl.git/edit/master/docs/index.md

[martintoreilly]

Fixed by:

• Setting edit_uri: edit/master/docs/src in docs/mkdocs.yaml [commit bcdb16b]. The edit_uri parameter is used by the underlying mkdocs utility the Julia Documenter package uses. The default value is edit/master/docs, but Documenter has source documents in docs/src rather than docs and does not appear to override edit_uri itself. Also set docs_dir: 'src' to match. This appears to be ignored byDocumenter but it is used if running mkdocs build directly.
• Setting repo_url: https://github.com/alan-turing-institute/PDMP.jl in docs/mkdocs.yaml [commit 806ce7d]. Removed .git extension which is not used in Github paths.
• Removing format = :html from docs/make.jl [commit 05515cb]. Default format is :markdown and theDocumenter deploydocs method seems to expect this format as Travis was not deploying to gh-pages branch when format was :html.