Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add configuration command #107

Closed
sharkdp opened this issue Jun 26, 2017 · 4 comments
Closed

Add configuration command #107

sharkdp opened this issue Jun 26, 2017 · 4 comments
Labels

Comments

@sharkdp
Copy link
Owner

sharkdp commented Jun 26, 2017

Some things came up that a user might want to configure:

  • number of significant digits that are displayed (default: 6)
  • decimal separator: . vs ,
  • terminal prompt
  • pretty printing: on/off
  • ...

I'd like to introduce a new keyword (e.g. set) that can control these:

> set displayed_digits 10
> set prompt "insect >>> "

Then, in a second step, we could read in a file like ~/.config/insectrc during startup where these settings (and user-defined variables) could be stored. For the web-version, settings could be stored in localStorage.

@sharkdp sharkdp added the idea label Jun 26, 2017
@sharkdp sharkdp mentioned this issue Jun 26, 2017
@leipert
Copy link

leipert commented Jun 26, 2017

IMO: we should keep the possible config parameters to a minimum.

@sharkdp
Copy link
Owner Author

sharkdp commented Mar 25, 2022

Released in v5.7.0

@sharkdp
Copy link
Owner Author

sharkdp commented Apr 2, 2022

Reopening for the set commands.

@triallax triallax changed the title Add configuration command and startup-file Add configuration command Jun 13, 2023
@sharkdp
Copy link
Owner Author

sharkdp commented Sep 26, 2023

Follow-up ticket for Numbat: sharkdp/numbat#97

@sharkdp sharkdp closed this as completed Sep 26, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants