Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support brief and extended docs (closes #25930) #34226

Merged
merged 3 commits into from Jan 25, 2020
Merged

Support brief and extended docs (closes #25930) #34226

merged 3 commits into from Jan 25, 2020

Commits on Jan 19, 2020

  1. Support brief and extended docs (closes #25930) 

    A level-1 header "Extended help" indicates that the content that follows
requires `??foo` rather than just `?foo`.
    @timholy
    timholy committed Jan 19, 2020
    Copy the full SHA
    4916589 View commit details
    Browse the repository at this point in the history

Commits on Jan 23, 2020

  1. Move extended docs handling to REPL

    @timholy
    timholy committed Jan 23, 2020
    Copy the full SHA
    3c6f01f View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2020

  1. Address review suggestions

    @timholy
    timholy committed Jan 24, 2020
    Copy the full SHA
    30c7ca0 View commit details
    Browse the repository at this point in the history