Skip to content

Commit

Permalink
feat(.travis.yml): export and run leanchecker
Browse files Browse the repository at this point in the history
This should detect multiple definitions with the same name as in #27.
  • Loading branch information
gebner authored and johoelzl committed Dec 14, 2017
1 parent 86e494d commit 0f50ba7
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,5 @@ install:

script:
- leanpkg test
- lean --recursive --export=mathlib.txt
- leanchecker mathlib.txt

0 comments on commit 0f50ba7

Please sign in to comment.