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

Re: Where does jshell save things

From	Arne Vajhøj <arne@vajhoej.dk>
Newsgroups	comp.lang.java.programmer
Subject	Re: Where does jshell save things
Date	2019-07-30 20:04 -0400
Organization	Aioe.org NNTP Server
Message-ID	<qhqlts$dd0$1@gioia.aioe.org> (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:
> Arne Vajhøj <arne@vajhoej.dk> writes:
> 
>> On 7/29/2019 2:59 PM, Cecil Westerhof wrote:
>>> When I start jshell it remembers the history from previous runs. Where
>>> is this saved?
>>
>> I believe it uses preferences API.
>>
>> So it is OS specific.
>>
>> Windows => registry
>>
>> *nix => $HOME/.java dir
> 
> I already thought about that, but in ~/.java I saw only a fonts
> directory. Looking better there is also an .userPrefs directory.
> (First time I see a hidden directory in a hidden directory.) 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.

-Djava.util.prefs.userRoot=.

should move the file to current dir.

And:

-Djava.util.prefs.PreferencesFactory=something

should allow you to use your entirely own preferences repo.

Arne

Back to comp.lang.java.programmer | Previous | Next — Previous 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