Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitattributes
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ RELEASES.md merge=union
stage0/** binary linguist-generated
# The following file is often manually edited, so do show it in diffs
stage0/src/stdlib_flags.h -binary -linguist-generated
doc/std/grove/GroveStdlib/Generated/** linguist-generated
# These files should not have line endings translated on Windows, because
# it throws off parser tests. Later lines override earlier ones, so the
# runner code is still treated as ordinary text.
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/grove.yml
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ jobs:
workflow: ci.yml
path: artifacts
name: "build-Linux release"
allow_forks: true
name_is_regexp: true

- name: Unpack toolchain
Expand Down
2 changes: 2 additions & 0 deletions doc/std/grove/GroveStdlib/Generated.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import GroveStdlib.Generated.«associative-creation-operations»
import GroveStdlib.Generated.«associative-modification-operations»
import GroveStdlib.Generated.«associative-create-then-query»
import GroveStdlib.Generated.«associative-all-operations-covered»
import GroveStdlib.Generated.«slice-producing»

/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
Expand All @@ -20,3 +21,4 @@ def restoreState : RestoreStateM Unit := do
«associative-modification-operations».restoreState
«associative-create-then-query».restoreState
«associative-all-operations-covered».restoreState
«slice-producing».restoreState
Loading
Loading