Skip to content
Snippets Groups Projects
Commit 996e6018 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Revert "Create Toolbox's workspace in user.home/.tlaplus."

This reverts commit 85628f37.

See https://github.com/tlaplus/tlaplus/issues/8 for context.
parent 516b500c
No related branches found
No related tags found
No related merge requests found
......@@ -34,7 +34,6 @@ openFile
<vmArgs>-Xmx1000m
-Dorg.eclipse.equinox.http.jetty.http.port=10996
-Dosgi.splashPath=platform:/base/
-Dosgi.instance.area.default=@user.home/.tlaplus/
</vmArgs>
<vmArgsMac>-XstartOnFirstThread -Dorg.eclipse.swt.internal.carbon.smallFonts
</vmArgsMac>
......@@ -57,6 +56,7 @@ openFile
<windows include="false">org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7</windows>
</vm>
<plugins>
</plugins>
......
......@@ -6,6 +6,20 @@ chmod 755 /opt/TLA+Toolbox/toolbox
## Update mime database for x-tla type.
/usr/bin/update-mime-database /usr/share/mime
## Place Toolbox's workspace directory
## in her home directory to support
## multi-user installation and not
## require user write access to
## /opt/TLA+Toolbox/. Also makes
## replacing the Toolbox less error
## prone when TLA+Toolbox is never
## touched except for dpkg.
## Having a fixed workspace location
## is also better than creating a
## workspace directory in ever directory
## from which the Toolbox is launched.
echo "-Dosgi.instance.area.default=@user.home/.tlaplus/" >> /opt/TLA+Toolbox/toolbox.ini
#- Apt repo
#-- Jenkins Plugin
#-- https://github.com/theoweiss/apt-repo
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment