leanprover / leanprover/fp-lean
Section 2.4, echo command doesn't work in `zsh`
Open
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 192
- Forks
- 73
- PR merge metrics
- No merged PRs in 30d
Description
Please quote the text that is incorrect:
echo "It works!" | ./build/bin/feline
In what way is this incorrect?
This works in bash, but in VS Code, the default has now become zsh, which yields an error (because of an interplay between the double quote and the !). Some possible fixes:
echo "It works" | ./build/bin/feline
echo ""It works!"" | ./build/bin/feline
echo 'It works!' | ./build/bin/feline
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Find the documentation for Section 2.4 and review the quoted echo command in a zsh shell, especially the interaction between double quotes and the exclamation mark. Update the example so it works in zsh, then verify the corrected command and ensure the surrounding explanation matches it.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- zsh
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 1/5
- Estimated time
- Under an hour
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 50/100