From de82d373be95a568279f318877760bf7ae11a7e4 Mon Sep 17 00:00:00 2001 From: jmoenig Date: Thu, 25 Jun 2015 16:35:00 +0200 Subject: [PATCH] add indentation again to please old.jslint.com :-) --- gui.js | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/gui.js b/gui.js index f7118475..eee2bd51 100644 --- a/gui.js +++ b/gui.js @@ -5040,9 +5040,9 @@ ProjectDialogMorph.prototype.shareProject = function () { if (proj.ProjectName === ide.projectName) { var usr = SnapCloud.username, projectId = 'Username=' + - encodeURIComponent(usr.toLowerCase()) + - '&ProjectName=' + - encodeURIComponent(proj.projectName); + encodeURIComponent(usr.toLowerCase()) + + '&ProjectName=' + + encodeURIComponent(proj.projectName); location.hash = projectId; } },