From 2ff18ddea8f0ae5653eeb979afc5bc13a93f25b6 Mon Sep 17 00:00:00 2001 From: Slava Pestov Date: Thu, 27 Mar 2008 17:12:47 -0500 Subject: [PATCH] Fix editors.jedit --- extra/editors/jedit/jedit.factor | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) mode change 100644 => 100755 extra/editors/jedit/jedit.factor diff --git a/extra/editors/jedit/jedit.factor b/extra/editors/jedit/jedit.factor old mode 100644 new mode 100755 index 7b6066df7c..92320addef --- a/extra/editors/jedit/jedit.factor +++ b/extra/editors/jedit/jedit.factor @@ -8,7 +8,7 @@ io.encodings.utf8 ; IN: editors.jedit : jedit-server-info ( -- port auth ) - home "/.jedit/server" append-path ascii [ + home ".jedit/server" append-path ascii [ readln drop readln string>number readln string>number