| commit | 0a3d6060d53da872729997807e1f564dbbb8c550 | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Thu Aug 01 15:07:00 2002 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Thu Aug 01 15:07:00 2002 +0000 |
| tree | 5ad8d20c6182798e36708620dde3b430b0a8a051 | |
| parent | 0dbab4c560c944956e4b732fe33ba0d72a8fb6df [diff] |
Only show the UI for selecting options if the ALT key was depressed while dragging or double-clicking the script.