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

Fix code location when reading history from a file #3416

Merged
merged 3 commits into from
Aug 21, 2024
Merged

Fix code location when reading history from a file #3416

merged 3 commits into from
Aug 21, 2024

Commits on Aug 18, 2024

  1. Add historyLength() compiled function 

    Returns value of history_length variable from readline history.
    @d-torrance
    d-torrance committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    ad419a3 View commit details
    Browse the repository at this point in the history

  2. Save history length at startup and use it to compute code location 

    When reading the history from a file, we need to add the number of
lines loaded from previous sessions when calling getHistory to get the
correct lines of code.

Closes: Macaulay2#3415
    @d-torrance
    d-torrance committed Aug 18, 2024
    Configuration menu
    Copy the full SHA
    6026326 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2024

  1. Don't use addStartFunction for setting up history; not necessary

    @d-torrance
    d-torrance committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    8724036 View commit details
    Browse the repository at this point in the history