gui/graph_displayer_canvas-edge.cc
changeset 1727 0c7d717b9538
parent 1643 9285f3777553
child 1731 616bc933c2bc
equal deleted inserted replaced
13:de3028325d67 14:feeddff356fe
   120 {
   120 {
   121   //the number in the map will be written on the edge
   121   //the number in the map will be written on the edge
   122   //EXCEPT when the name of the map is Default, because
   122   //EXCEPT when the name of the map is Default, because
   123   //in that case empty string will be written, because
   123   //in that case empty string will be written, because
   124   //that is the deleter map
   124   //that is the deleter map
   125 
   125   
   126   if(edge==INVALID)
   126   if(edge==INVALID)
   127     {
   127     {
   128       for (EdgeIt i(mapstorage.graph); i!=INVALID; ++i)
   128       for (EdgeIt i(mapstorage.graph); i!=INVALID; ++i)
   129 	{
   129 	{
   130 	  if(mapname!="Default")
   130 	  if(mapname!="Default")