Add save edge and reuse it.

This commit is contained in:
Oleg Sh
2023-01-07 19:59:48 +02:00
parent 168a851b75
commit b6065ef901
17 changed files with 247 additions and 86 deletions

View File

@@ -196,6 +196,8 @@ var g_reverseAllEdges = "Reverse all edges";
var g_makeAllUndirected = "Make all edges undirected";
var g_makeAllDirected = "Make all edges directed";
var g_reuseSavedEdge = "Reuse saved edge";
function loadTexts()
{
g_textsSelectAndMove = document.getElementById("SelectAndMoveObject").innerHTML;
@@ -399,5 +401,7 @@ function loadTexts()
g_makeAllDirected = document.getElementById("makeAllDirected").innerHTML;
g_pairWrongFormat = document.getElementById("pairWrongFormat").innerHTML;
g_fix = document.getElementById("fixButton").innerHTML;;
g_fix = document.getElementById("fixButton").innerHTML;
g_reuseSavedEdge = document.getElementById("reuseSavedEdge").innerHTML;
}