1.1 --- a/gui/graph-displayer.cc	Fri Jun 17 14:53:28 2005 +0000
     1.2 +++ b/gui/graph-displayer.cc	Fri Jun 17 15:41:48 2005 +0000
     1.3 @@ -15,12 +15,12 @@
     1.4  
     1.5    //initializing
     1.6  
     1.7 -  //  property_strings=new std::string[PROPERTY_NUM];
     1.8 +  property_strings.resize(PROPERTY_NUM);
     1.9    property_strings[WIDTH]="Width";
    1.10    property_strings[COLOR]="Color";
    1.11    property_strings[TEXT]="Text";
    1.12  
    1.13 -  //property_defaults=new double[PROPERTY_NUM];
    1.14 +  property_defaults.resize(PROPERTY_NUM);
    1.15    property_defaults[WIDTH]=10.0;
    1.16    property_defaults[COLOR]=100;
    1.17    property_defaults[TEXT]=0;