graph_displayer_canvas-edge.cc
branchgui
changeset 47 9a0e6e92d06c
parent 45 199f433eb7cd
child 48 b8ec84524fa2
     1.1 --- a/graph_displayer_canvas-edge.cc	Wed Jul 27 11:35:13 2005 +0000
     1.2 +++ b/graph_displayer_canvas-edge.cc	Thu Jul 28 14:31:32 2005 +0000
     1.3 @@ -22,7 +22,7 @@
     1.4  	  int w=(int)(*actual_map)[i];
     1.5  	  if(w>=0)
     1.6  	    {
     1.7 -	      edgesmap[i]->property_width_pixels().set_value(w);
     1.8 +	      edgesmap[i]->property_width_units().set_value(w);
     1.9  	    }
    1.10  	}
    1.11      }
    1.12 @@ -31,7 +31,7 @@
    1.13        int w=(int)(*actual_map)[edge];
    1.14        if(w>=0)
    1.15  	{
    1.16 -	  edgesmap[edge]->property_width_pixels().set_value(w);
    1.17 +	  edgesmap[edge]->property_width_units().set_value(w);
    1.18  	}
    1.19      }
    1.20    return 0;