Skip to content
This repository has been archived by the owner on Jul 19, 2022. It is now read-only.

Fix bug where builtin folds were not disabled #279

Merged
merged 1 commit into from
Nov 29, 2021

Conversation

hojberg
Copy link
Member

@hojberg hojberg commented Nov 24, 2021

Overview

Builtins can be unfolded, and the fold toggle should be disabled.

Fixes #266

Builtins can be unfolded, and the fold toggle should be disabled.
@hojberg hojberg merged commit 105a4b9 into main Nov 29, 2021
@hojberg hojberg deleted the ensure-builtin-fold-is-disabled branch November 29, 2021 15:24
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Builtin terms shouldn't have a "expand" interaction
1 participant