diff --git a/src/plugins/wp/share/.gitignore b/src/plugins/wp/share/.gitignore index c2552132a1cd74d94aae607ec90a7dcc7875639f..b4928767a3aee4ccf044d41181f91359c950cc59 100644 --- a/src/plugins/wp/share/.gitignore +++ b/src/plugins/wp/share/.gitignore @@ -1,18 +1,6 @@ -/ergo/*.mlw.bak -/why3/why3.conf -/why3/*.why.bak -/why3/*.vo -/why3/*.glob -/why3/.*.aux -/why3/.depend -/coqwp/.depend -/coqwp/*/*.vo -/coqwp/*/*.glob -/coqwp/*.vo -/coqwp/*.glob -/coqwp/.*.aux -/coqwp/*/.*.aux -/.depend +*.vo +*.glob +*.aux /instwp /install /html