Ignore profiling output filetypes.
commit665181ced669dac3468938aaf2c599157ad3a002
authorNicolas Wu <nick@well-typed.com>
dateTue 31 Jan 2012, 11:03 (15 years ago)
parent6cf44a5
.gitignore+4
@@ -3,5 +3,9 @@ TAGS
33dist/
44\#*#
55*~
6+*.aux
7+*.hp
68*.hi
79*.o
10+*.prof
11+*.ps