From 87329289d7a9bcfc2bd84a7c419e172e153f1ea3 Mon Sep 17 00:00:00 2001
From: Sylvain Pion <Sylvain.Pion@sophia.inria.fr>
Date: Sun, 21 May 2006 22:32:27 +0000
Subject: [PATCH] Replace src_CGAL/ by Number_types/

---
 Scripts/test/collect_cgal_testresults | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Scripts/test/collect_cgal_testresults b/Scripts/test/collect_cgal_testresults
index 70a06901e74..170e9d83d9a 100755
--- a/Scripts/test/collect_cgal_testresults
+++ b/Scripts/test/collect_cgal_testresults
@@ -11,7 +11,7 @@
 
 print_platforms()
 {
-  cd src_CGAL
+  cd Number_types  # Pick a stable directory at random
   for FILE in `ls CompilerOutput_*` ; do
     PLATFORM=`echo $FILE | sed 's/CompilerOutput_//'| sed 's/\.gz//'`
     printf "$PLATFORM "