Gnome and broken buttons - Revision history

imported>Nicolas: /* Script */

2010-02-03T13:25:32Z

Script

← Older revision		Revision as of 13:25, 3 February 2010
Line 52:		Line 52:

	A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.		A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.

			Note: the script has been added to official Rodin releases (1.2+) for Linux.

imported>Nicolas: /* Script */

2010-02-03T11:23:31Z

Script

← Older revision		Revision as of 11:23, 3 February 2010
Line 21:		Line 21:
	1. create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)		1. create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)

	2. copy/paste the following ~~script~~:		2. copy/paste one of the following scripts (both should work; if one does not, just try the other one) :

			#!/bin/sh
			GDK_NATIVE_WINDOWS=1
			export GDK_NATIVE_WINDOWS

			# Compute directory prefix
			case "$0" in
			/) DIR="`dirname \"$0\"`/" ;;
			*) DIR=""
			esac

			"${DIR}rodin" "$@"

	#!/bin/sh		#!/bin/sh
Line 32:		Line 44:

	"$RODIN_CMD" "$@"		"$RODIN_CMD" "$@"

	3. make the file executable:		3. make the file executable:
	chmod +x rodin.sh		chmod +x rodin.sh

imported>Nicolas: /* Script */ fixed script to consider paths with spaces

2010-02-03T11:02:34Z

Script: fixed script to consider paths with spaces

← Older revision		Revision as of 11:02, 3 February 2010
Line 27:		Line 27:
	export GDK_NATIVE_WINDOWS		export GDK_NATIVE_WINDOWS

	SCRIPT_PATH=$(readlink -f $0)		SCRIPT_PATH=$(readlink -f "$0")
	RODIN_DIR=$(dirname $SCRIPT_PATH)		RODIN_DIR=$(dirname "$SCRIPT_PATH")
	RODIN_CMD=$RODIN_DIR/rodin		RODIN_CMD="$RODIN_DIR"/rodin

	$RODIN_CMD "$@"		"$RODIN_CMD" "$@"
	3. make the file executable:		3. make the file executable:
	chmod +x rodin.sh		chmod +x rodin.sh

imported>Nicolas: /* Workaround */

2010-01-18T17:23:02Z

Workaround

← Older revision		Revision as of 17:23, 18 January 2010
Line 13:		Line 13:
	* /etc/profile (requires root privileges)		* /etc/profile (requires root privileges)
	* ~/.bashrc if you intend to start rodin always from a terminal		* ~/.bashrc if you intend to start rodin always from a terminal

			However, the OS tends to override the value of this variable.

	===Script===		===Script===

imported>Nicolas at 18:24, 15 January 2010

2010-01-15T18:24:45Z

← Older revision		Revision as of 18:24, 15 January 2010
Line 14:		Line 14:
	* ~/.bashrc if you intend to start rodin always from a terminal		* ~/.bashrc if you intend to start rodin always from a terminal

			===Script===
	Another way to go is to create a shell script that will initialize the variable and start rodin. Then you will have to use the script instead of the executable.		Another way to go is to create a shell script that will initialize the variable and start rodin. Then you will have to use the script instead of the executable.
	* create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)
	* copy/paste the following script:		1. create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)

			2. copy/paste the following script:

	#!/bin/sh		#!/bin/sh
	GDK_NATIVE_WINDOWS=1		GDK_NATIVE_WINDOWS=1
Line 26:		Line 30:

	$RODIN_CMD "$@"		$RODIN_CMD "$@"
	* make the file executable:		3. make the file executable:
	chmod +x rodin.sh		chmod +x rodin.sh
	* start rodin from the script:		4. start rodin from the script:
	./rodin.sh		./rodin.sh
	You may also make shortcuts point to this script.		You may also make shortcuts point to this script.

	A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.		A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.

imported>Nicolas: New page: A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenced all over the Web in bug reports and forums, fo...

2010-01-15T18:16:11Z

New page: A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenced all over the Web in bug reports and forums, fo...

New page

A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenced all over the Web in bug reports and forums, for instance [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257|here]].

==Workaround==

The general workaround (besides waiting for a correction of the bug in GTK), consists in setting a GDK_NATIVE_WINDOWS environment variable to 1 (or true) before starting rodin:

export GDK_NATIVE_WINDOWS=1
/path_to_rodin/rodin

directly in command line.

An alternative is to make it permanent by setting the variable in a configuration file:
* /etc/profile (requires root privileges)
* ~/.bashrc if you intend to start rodin always from a terminal

Another way to go is to create a shell script that will initialize the variable and start rodin. Then you will have to use the script instead of the executable.
* create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)
* copy/paste the following script:
#!/bin/sh
GDK_NATIVE_WINDOWS=1
export GDK_NATIVE_WINDOWS

SCRIPT_PATH=$(readlink -f $0)
RODIN_DIR=$(dirname $SCRIPT_PATH)
RODIN_CMD=$RODIN_DIR/rodin

$RODIN_CMD "$@"
* make the file executable:
chmod +x rodin.sh
* start rodin from the script:
./rodin.sh
You may also make shortcuts point to this script.

A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.