Skip to content

Commit

Permalink
[goal-view] Correct unshelve message
Browse files Browse the repository at this point in the history
  • Loading branch information
rtetley committed Aug 5, 2024
1 parent a32ace3 commit 5755811
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,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 5755811

Please sign in to comment.