SOURCES: jspin-config.patch (NEW) - fix windows-centric config settings

[baggins]

Author: baggins                      Date: Mon Feb 16 13:49:42 2009 GMT
Module: SOURCES                       Tag: HEAD
---- Log message:
- fix windows-centric config settings

---- Files affected:
SOURCES:
   jspin-config.patch (NONE -> 1.1)  (NEW)

---- Diffs:

================================================================
Index: SOURCES/jspin-config.patch
diff -u /dev/null SOURCES/jspin-config.patch:1.1
--- /dev/null	Mon Feb 16 14:49:43 2009
+++ SOURCES/jspin-config.patch	Mon Feb 16 14:49:37 2009
@@ -0,0 +1,58 @@
+--- jspin-4.6/config.cfg~	2008-09-29 08:28:52.000000000 +0200
++++ jspin-4.6/config.cfg	2009-02-16 14:43:48.299335175 +0100
+@@ -8,13 +8,13 @@
+ SELECT_MENU=5
+ WRAP=true
+ SELECT_BUTTON=220
+-SPIN=bin\\spin.exe
++SPIN=@@BINDIR@@/spin
+ LR_DIVIDER=400
+ CHECK_OPTIONS=-a -v
+ VERIFY_MODE=Safety
+ VARIABLE_WIDTH=10
+ MSC=false
+-SOURCE_DIRECTORY=jspin-examples
++SOURCE_DIRECTORY=@@EXAMPLESDIR@@/jspin-examples
+ TAB_SIZE=4
+ RAW=false
+ C_COMPILER_OPTIONS=-o pan pan.c
+@@ -22,13 +22,13 @@
+ TRAIL_OPTIONS=-t -X
+ MAX_DEPTH=2000
+ TRANSLATE_OPTIONS=-f
+-C_COMPILER=c\:\\mingw\\bin\\gcc.exe
++C_COMPILER=/usr/bin/gcc
+ STATEMENT_TITLE=Statement 
+-DOT=bin\\dot.exe
+-ABOUT_FILE_NAME=txt\\copyright.txt
++DOT=/usr/bin/dot
++ABOUT_FILE_NAME=copyright.txt
+ FONT_STYLE=0
+ MIN_DIVIDER=50
+-HELP_FILE_NAME=txt\\help.txt
++HELP_FILE_NAME=help.txt
+ PROCESS_TITLE=Process 
+ HEIGHT=700
+ SINGLE_QUOTE=false
+--- jspin-4.6/jspin/Config.java~	2008-09-29 08:05:26.000000000 +0200
++++ jspin-4.6/jspin/Config.java	2009-02-16 14:43:45.022673099 +0100
+@@ -26,13 +26,13 @@
+ 
+     static void setDefaultProperties() {
+         // Directories and file names
+-        properties.put("SOURCE_DIRECTORY", "jspin-examples");
+-        properties.put("C_COMPILER",       "c:\\mingw\\bin\\gcc.exe");
+-        properties.put("SPIN",             "bin" + sep + "spin.exe");
++        properties.put("SOURCE_DIRECTORY", "@@EXAMPLESDIR@@/jspin-examples");
++        properties.put("C_COMPILER",       "/usr/bin/gcc");
++        properties.put("SPIN",             "@@BINDIR@@/spin");
+         properties.put("PAN",              "pan");
+-        properties.put("DOT",              "bin" + sep + "dot.exe");
+-        properties.put("HELP_FILE_NAME",   "txt" + sep + "help.txt");
+-        properties.put("ABOUT_FILE_NAME",  "txt" + sep + "copyright.txt");
++        properties.put("DOT",              "@@BINDIR@@/dot");
++        properties.put("HELP_FILE_NAME",   "help.txt");
++        properties.put("ABOUT_FILE_NAME",  "copyright.txt");
+ 
+         // Options for executing Spin
+         properties.put("SINGLE_QUOTE", Boolean.toString(false));
================================================================