Skip to content

Commit

Permalink
Merge pull request #854 from coq-community/unshelve-typos
Browse files Browse the repository at this point in the history
Correct unshelve message
  • Loading branch information
rtetley authored Aug 5, 2024
2 parents 2880bd8 + 5755811 commit 996bbf6
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.main)}
displaySetting={displaySetting}
emptyMessage={
goals!.shelved.length ? "There are shelved goals. Try using unshelved" :
goals!.shelved.length ? "There are shelved goals. Try using `Unshelve.`" :
goals!.givenUp.length ? "There are some goals you gave up. Go back and solve them, or use `Admitted.`" :
"There are no more subgoals"
}
Expand Down

0 comments on commit 996bbf6

Please sign in to comment.