Skip to content

Commit

Permalink
chore: move tutorial to examples folder
Browse files Browse the repository at this point in the history
  • Loading branch information
Vtec234 committed Aug 3, 2022
1 parent dd73d87 commit 4bdab83
Show file tree
Hide file tree
Showing 3 changed files with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@
- [Frequently Asked Questions](./faq.md)
- [Significant Changes from Lean 3](./lean3changes.md)
- [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
- [User Widgets](./widgets.md)
- [User Widgets](examples/widgets.lean.md)

# Development

Expand Down
File renamed without changes.
File renamed without changes.

0 comments on commit 4bdab83

Please sign in to comment.