rolandschulz/PTP — Issue #59: Remove filtered files from repository
Author: eblen
Created: 2012-03-08 22:34:53+00:00
State: open
Labels: Medium priority, Non-trivial

Filtered files should be removed from the git repository, so that their last unfiltered versions do not appear for new configurations. (There may be other problems caused by this too.)