+ docstring const label = getParam("name");
+ if (buffer().params().output_changes
+ && buffer().activeLabel(label)
+ && buffer().insetLabel(label, true) != this) {
+ // this is a deleted label and we have a non-deleted with the same id
+ // rename it for output to prevent wrong references
+ docstring newlabel = label;
+ int i = 1;
+ while (buffer().insetLabel(newlabel)) {
+ newlabel = label + "-DELETED-" + convert<docstring>(i);
+ ++i;
+ }
+ command = subst(command, label, newlabel);
+ }