Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.java.programmer > #39024

Re: Where does jshell save things

From Eric Sosman <esosman@comcast-dot-net.invalid>
Newsgroups comp.lang.java.programmer
Subject Re: Where does jshell save things
Date 2019-07-30 07:11 -0400
Organization A noiseless patient Spider
Message-ID <qhp8li$n76$1@dont-email.me> (permalink)
References <87lfwgoeez.fsf@munus.decebal.nl> <qho0v8$2j4$1@gioia.aioe.org> <87d0hsnla8.fsf@munus.decebal.nl>

Show all headers | View raw


On 7/30/2019 1:28 AM, Cecil Westerhof wrote:
> [...]   The file
> I need is:
>      ~/.java/.userPrefs/tool/JShell/prefs.xml
> 
> I do not like that it is XML, but it is what it is.

     Since you're using a Unixoid system, just construct a named
pipe that connects to an XML-to-JSON and JSON-to-XML translator.
(For "JSON," substitute your preferred format.)

     Problem solved!  ;-)

-- 
esosman@comcast-dot-net.invalid
Five hundred forty days to go.

Back to comp.lang.java.programmer | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread


Thread

Where does jshell save things Cecil Westerhof <Cecil@decebal.nl> - 2019-07-29 20:59 +0200
  Re: Where does jshell save things Arne Vajhøj <arne@vajhoej.dk> - 2019-07-29 19:54 -0400
    Re: Where does jshell save things Cecil Westerhof <Cecil@decebal.nl> - 2019-07-30 07:28 +0200
      Re: Where does jshell save things Eric Sosman <esosman@comcast-dot-net.invalid> - 2019-07-30 07:11 -0400
      Re: Where does jshell save things Arne Vajhøj <arne@vajhoej.dk> - 2019-07-30 20:04 -0400

csiph-web