Code

Ignore errors when completing#39

Code

Merged

gallais merged 1 commit intoidris-community:mainidris-community/idris2-mode:mainfrom jeroendehaas:fix-completion-errorjeroendehaas/idris2-mode:fix-completion-errorCopy head branch name to clipboardDec 20, 2024

+17-14

Commits

Commits on Jan 9, 2023

• Ignore errors when completing

  jeroendehaas

  committed
  3567047

  Copy full SHA for 3567047