Closed mitchellwrosen closed 1 month ago
This PR adds a variant of edit (codename edit2) that adds definitions to the top of the file without a fold line below them. It's also careful not to add definitions that already exist in the latest typechecked file.
edit
edit2
I've tested this manually and added a transcript.
Rename edit2 to ?
Let's have edit.new be the existing behavior of adding the fold, edit be the new behavior that does not add a fold, like you'd originally suggested.
edit.new
@aryairani this is ready to go
Overview
This PR adds a variant of
edit
(codenameedit2
) that adds definitions to the top of the file without a fold line below them. It's also careful not to add definitions that already exist in the latest typechecked file.Test coverage
I've tested this manually and added a transcript.
Loose ends
Rename
edit2
to ?