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

Add a command to delete history item at point #3574

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Add a command to delete history item at point #3574

wants to merge 7 commits into from

Commits on Nov 10, 2023

  1. Store history on a per-project basis by default

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    c9c2a6b View commit details
    Browse the repository at this point in the history

  2. Really share the histories when `cider-repl-history-file' is set

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    b7a5c4d View commit details
    Browse the repository at this point in the history

  3. Set the name of the local history file according to the REPL type

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    132bcc4 View commit details
    Browse the repository at this point in the history

  4. Stop merging the input history with `cider-repl-history-file' 

    Because input history cannot be changed by another REPL anymore
    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    2bbe784 View commit details
    Browse the repository at this point in the history

  5. Find a suitable directory to store the local history to more robustly

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    3d001d7 View commit details
    Browse the repository at this point in the history

  6. Calculate the length of the history only once

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    959e5d3 View commit details
    Browse the repository at this point in the history

  7. Add a command to delete history item at point

    @Zzull
    Zzull committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    41cccdf View commit details
    Browse the repository at this point in the history