Appearance
Configuration Page
The Configuration Page is used to create and edit custom shell scripts and configuration files, configure your IDE and define personal workspace startup scripts. You can also configure additional settings (e.g. theme) by clicking on the profile picture on the top right of the screen.
Configuration Files
Personal configuration files can be managed from the Profile Settings. These files can be injected in any new or existing workspaces automatically using the ... icon and the option personalize environment.
You can edit and manage typical shell scripts attached to Linux-based environments such as:
- .bashrc,
- .zshrc,
- .profile, or any file of your choice using the
- custom: option.
IDE Configuration
IDE configuration files can be managed from the profile settings. A configuration must be initially imported from a running workspaces. Then, it can be applied a new or existing workspaces manually or automatically.
Currently supported IDEs are:
- VSCode,
- any IDEs from Jetbrains.
Startup Script
You can define a personal script that will be executed upon each startup of the workspaces that you own
TIP
note that if you defined a startup script for a given workspace, then it will override this one
Theme
Two color themes for dashboards are available in the Profile Menu. You can switch between a light and dark them for the User Interface (UI) display.
Language
A language for the UI can be selected from the footer. Supported languages for the platform UI are:
- English,
- French.