added s/selectI/someI/g;
authorwenzelm
Fri, 15 Sep 2000 20:19:24 +0200
changeset 9996 dede9cf1bd2a
parent 9995 8414454c8e11
child 9997 38598a19e701
added s/selectI/someI/g;
lib/scripts/fixsome.pl
--- a/lib/scripts/fixsome.pl	Fri Sep 15 20:18:36 2000 +0200
+++ b/lib/scripts/fixsome.pl	Fri Sep 15 20:19:24 2000 +0200
@@ -19,6 +19,7 @@
     s/select_eq_Ex/some_eq_ex/g;
     s/selectI2EX/someI2_ex/g;
     s/selectI2/someI2/g;
+    s/selectI/someI/g;
     s/select1_equality/some1_equality/g;
     s/Eps_sym_eq/some_sym_eq_trivial/g;
     s/Eps_eq/some_eq_trivial/g;