update gitignore

Authored by dterei on Jan 17 2013, 3:17 AM.

Description

update gitignore

Details

Committed
dtereiJan 17 2013, 3:17 AM
Pushed
bgamariAug 25 2016, 1:39 PM
Parents
rGHCDIFF18fd170a85d9: Test for #7600.
Branches
Unknown
Tags
Unknown