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;