Code

Fix #6377: Change ctrl-r shortcut#6620

Code

Merged

mergify[bot] merged 1 commit intodevelopenso-org/enso:developfrom wip/procrat/fix-ctrl-r-restore-6377enso-org/enso:wip/procrat/fix-ctrl-r-restore-6377Copy head branch name to clipboardMay 10, 2023

+14-5

Commits

Commits on May 9, 2023

• Fix #6377: Change ctrl-r shortcut

  Procrat

  committed
  3c053f6