gui/graph_displayer_canvas-edge.cc
changeset 1598 739df601808d
parent 1596 44897b1ba4e2
child 1599 c2f95eac652b
     1.1 --- a/gui/graph_displayer_canvas-edge.cc	Wed Jul 27 11:35:13 2005 +0000
     1.2 +++ b/gui/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;