# HG changeset patch
# User wenzelm
# Date 969041964 -7200
# Node ID dede9cf1bd2a115ff4a29855f8f40d11986ba7a7
# Parent  8414454c8e116703bb7a32394406df6bc05e2486
added s/selectI/someI/g;

diff -r 8414454c8e11 -r dede9cf1bd2a 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;