Anders Logg <[email protected]> writes: > Do you remember how? I could dig up the old scripts we used to clean > the repository. But wouldn't that lead to problems with all branches > merged off from master after those files were added?
You have merged to 'master' so you can't remove something without rewriting that history (causing everyone's work to not fast-forward and obliging them to reset any branches that weren't pushed at the time you ran 'git filter-branch' to rewrite history). Probably not worth it given the problem size. You can add the relevant suffixes to .gitignore if you don't want to accidentally commit them again.
pgpEBvWfda2oH.pgp
Description: PGP signature
_______________________________________________ fenics mailing list [email protected] http://fenicsproject.org/mailman/listinfo/fenics
