Skip to content

Commit

Permalink
Some files have where on their own lines.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Dec 16, 2024
1 parent 2b9f351 commit 7293394
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions lua/lean/indent.lua
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ local NEVER_INDENT = vim.regex(([[^\s*\(%s\)]]):format(table.concat({
'def ',
'instance ',
'structure ',
'where',
'@\\[',
}, [[\|]])))

Expand Down

0 comments on commit 7293394

Please sign in to comment.