Skip to content

Commit

Permalink
In .gitignore, stop ignoring no longer existing manual-related tools
Browse files Browse the repository at this point in the history
  • Loading branch information
@shindere
shindere committed Oct 13, 2022
1 parent aa0de73 commit 00b9167
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,10 +173,6 @@ META
/manual/tools/transf.ml
/manual/tools/texquote2
/manual/tools/transf
/manual/tools/htmlgen
/manual/tools/htmlquote
/manual/tools/latexscan.ml
/manual/tools/dvi2txt

/api_docgen/build
/api_docgen/odoc/build
Expand Down

0 comments on commit 00b9167

Please sign in to comment.