From eb0203510d359582426dbfa4504fd171b005f81d Mon Sep 17 00:00:00 2001 From: bourgeoa Date: Mon, 30 Jan 2023 16:32:35 +0100 Subject: [PATCH] setUnedited after save --- .eslintrc | 4 ---- src/sourcePane.js | 4 ++-- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/.eslintrc b/.eslintrc index eefc7f7..6c8ae66 100644 --- a/.eslintrc +++ b/.eslintrc @@ -1,8 +1,4 @@ { - /* "parserOptions": { - "ecmaVersion": 6, - "sourceType": "module" - }, */ "root": true, "env": { "browser": true, diff --git a/src/sourcePane.js b/src/sourcePane.js index ec58c72..d1cd87a 100644 --- a/src/sourcePane.js +++ b/src/sourcePane.js @@ -119,7 +119,7 @@ module.exports = { ) } - const myCompactButton = controls.appendChild(compactButton(dom)) // alain + const myCompactButton = controls.appendChild(compactButton(dom)) const cancelButton = controls.appendChild(UI.widgets.cancelButton(dom)) const saveButton = controls.appendChild(UI.widgets.continueButton(dom)) const myEditButton = controls.appendChild(editButton(dom)) @@ -247,7 +247,7 @@ module.exports = { const response = await fetcher.webOperation('HEAD', subject.uri, defaultFetchHeaders()) if (!happy(response, 'HEAD')) return getResponseHeaders(response) // get new eTag - setEdited() + setUnedited() // used to be setEdited() } catch (err) { throw err }