Skip to content

Commit e69fd43

Browse files
authored
remove latex_minted (#775)
1 parent e8317cf commit e69fd43

File tree

4 files changed

+0
-173
lines changed

4 files changed

+0
-173
lines changed

misc/latex_minted/.gitignore

Lines changed: 0 additions & 1 deletion
This file was deleted.

misc/latex_minted/dedukti.py

Lines changed: 0 additions & 73 deletions
This file was deleted.

misc/latex_minted/dedukti.sty

Lines changed: 0 additions & 7 deletions
This file was deleted.

misc/latex_minted/example.tex

Lines changed: 0 additions & 92 deletions
This file was deleted.

0 commit comments

Comments
 (0)