gui/graph_displayer_canvas-edge.cc
changeset 1579 ed7da82bbecf
parent 1525 6d94de269ab1
child 1581 9bb83c7f479b
     1.1 --- a/gui/graph_displayer_canvas-edge.cc	Wed Jul 20 22:36:37 2005 +0000
     1.2 +++ b/gui/graph_displayer_canvas-edge.cc	Thu Jul 21 19:28:29 2005 +0000
     1.3 @@ -118,6 +118,7 @@
     1.4  	{
     1.5  	  if(mapname!="Default")
     1.6  	    {
     1.7 +	      edgemap_to_edit=mapname;
     1.8  	      double number=(*(mapstorage.edgemap_storage)[mapname])[i];
     1.9  	      int length=1;
    1.10  	      //if number is smaller than one, length would be negative, or invalid
    1.11 @@ -146,6 +147,7 @@
    1.12  	    }
    1.13  	  else
    1.14  	    {
    1.15 +	      edgemap_to_edit="";
    1.16  	      edgetextmap[i]->property_text().set_value("");
    1.17  	    }
    1.18  	}