fix time extractor to parse names with spaces

git-svn-id: https://svn.dealii.org/trunk@28285 0785d39b-7218-0410-832d-ea1e28bc413d

diff --git a/tests/benchmarks/gettimes/get_times.cc b/tests/benchmarks/gettimes/get_times.cc
index 8018899cd2feb73744ab99635455e928ec46ecdf..41bc557a0c24502fb4fdf7112c46c9c1f59b0c34 100644 (file)
--- a/tests/benchmarks/gettimes/get_times.cc
+++ b/tests/benchmarks/gettimes/get_times.cc
@@ -50,17 +50,23 @@ int main(int argc, char *argv[]) {
                        if (curr_line[1] == ' ')
                                first_char++;
 
+                       
                        ////cout << "first char at pos: " << first_char << endl;
        
                        //Test case: char at position first_char is a letter
                        assert(isalpha(curr_line[first_char]));
                        
-                       //Find position of first space that occurs after the word
+                       //Find end of string
                        int num_chars = 0;
-                       while(!isspace(curr_line[first_char + num_chars]))
+                       while(curr_line[first_char + num_chars] != '|')
                                num_chars++;
-       
-                       names.push_back(curr_line.substr(first_char, num_chars));
+
+                       num_chars--;
+                       
+                       while(curr_line[first_char + num_chars] == ' ')
+                         num_chars--;
+                       
+                       names.push_back(curr_line.substr(first_char, num_chars+1));
                }
        }