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

Plant anchors for hunks to create links in doc preview changes #36742

Merged
merged 16 commits into from
Dec 10, 2023
Merged

Plant anchors for hunks to create links in doc preview changes #36742

merged 16 commits into from
Dec 10, 2023

Commits on Nov 21, 2023

  1. Plant anchors for hunks

    @kwankyu
    kwankyu committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    b9ceb3a View commit details
    Browse the repository at this point in the history

  2. Fix a typo

    @kwankyu
    kwankyu committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    aca1279 View commit details
    Browse the repository at this point in the history

Commits on Nov 24, 2023

  1. Split out script

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    99eb4f3 View commit details
    Browse the repository at this point in the history

  2. Error if wrong arguments

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    fed139e View commit details
    Browse the repository at this point in the history

  3. Make script name right

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    0265da1 View commit details
    Browse the repository at this point in the history

  4. Fix help text

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    380cc8e View commit details
    Browse the repository at this point in the history

  5. Fix indentation

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    e8a63ab View commit details
    Browse the repository at this point in the history

  6. Separate the script more

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    b637cc1 View commit details
    Browse the repository at this point in the history

  7. Remove ./docs prefix

    @kwankyu
    kwankyu committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    65a5e01 View commit details
    Browse the repository at this point in the history

Commits on Nov 25, 2023

  1. Use system python

    @kwankyu
    kwankyu committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    bd423eb View commit details
    Browse the repository at this point in the history

  2. Supply Sage root

    @kwankyu
    kwankyu committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    00778d7 View commit details
    Browse the repository at this point in the history

  3. There are 3 arguments to the script

    @kwankyu
    kwankyu committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    e124281 View commit details
    Browse the repository at this point in the history

  4. Better solution for using python

    @kwankyu
    kwankyu committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    ac82ac4 View commit details
    Browse the repository at this point in the history

Commits on Nov 26, 2023

  1. Remove

    @kwankyu
    kwankyu committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    e1388ba View commit details
    Browse the repository at this point in the history

  2. This seems to make a difference

    @kwankyu
    kwankyu committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    976c1b3 View commit details
    Browse the repository at this point in the history

  3. Second attempt

    @kwankyu
    kwankyu committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    7b0c670 View commit details
    Browse the repository at this point in the history