Code

Abbreviations Manager#3202

Code

Open

wadoon wants to merge 10 commits intomainKeYProject/key:mainfrom weigl/abbrevmgrKeYProject/key:weigl/abbrevmgrCopy head branch name to clipboard

+1,022-802

Commits

Commits on Jul 14, 2023

• first version some bugs to fix

  wadoon

  committed
  4c3fb6c

  Copy full SHA for 4c3fb6c

• use pretty printer for abbreviation mapping files

  wadoon

  committed
  2c3a88e

  Copy full SHA for 2c3a88e

Commits on Jul 16, 2023

• Refactor SequentViewMenu & Co

  wadoon

  committed
  25e2672

  Copy full SHA for 25e2672

Commits on Aug 21, 2023

• Merge remote-tracking branch 'origin/main' into weigl/abbrevmgr

  wadoon

  committed
  4f4770d

  Copy full SHA for 4f4770d

• Merge remote-tracking branch 'origin/main' into weigl/abbrevmgr

  Show description for 5c7e4d2
  wadoon

  committed
  5c7e4d2

  Copy full SHA for 5c7e4d2

Commits on Nov 19, 2023

• Merge remote-tracking branch 'origin/main' into weigl/abbrevmgr

  Show description for 939225b
  wadoon

  committed
  939225b

  Copy full SHA for 939225b

• Merge errors (jspecify)

  wadoon

  committed
  96e42b9

  Copy full SHA for 96e42b9

Commits on Nov 27, 2023

• Merge branch 'main' into weigl/abbrevmgr

  wadoon

  authored
  d1c072a

  Copy full SHA for d1c072a

Commits on Dec 3, 2023

• Merge branch 'main' into weigl/abbrevmgr

  wadoon

  authored
  ee98653

  Copy full SHA for ee98653

Commits on Feb 3, 2024

• Merge branch 'main' into weigl/abbrevmgr

  wadoon

  authored
  6a80690

  Copy full SHA for 6a80690