Exclude plfa.github.io-web-* folders from Jekyll build.
This commit is contained in:
parent
ccda5c009e
commit
2ef6e73ecb
1 changed files with 1 additions and 0 deletions
|
@ -60,6 +60,7 @@ exclude:
|
|||
- "papers/"
|
||||
- "slides/"
|
||||
- "vendor/"
|
||||
- "plfa.github.io-web-*/"
|
||||
- "*.agdai"
|
||||
- "*.agda-lib"
|
||||
- "*.lagda.md"
|
||||
|
|
Loading…
Reference in a new issue