Merge branch 'devel' into feature-ga

diff --cc .gitignore
index b2a5628,d5a15a6..521532d
--- 1/.gitignore
--- 2/.gitignore
+++ b/.gitignore
@@@ -1,2 -1,19 +1,20 @@@
+ # ignore compiled stuff
+ *.[oa]
+ 
+ # ignore texteditors
  *.swp
+ *~
+ 
+ # ignore PBS output and error files
+ *.[eo][0-9][0-9][0-9][0-9]*
+ 
+ # ignore build dir
+ build/
 +source/ga/build
+ 
+ # ignored dirs form adasko
+ gradcheck/
+ mapcheck/
+ run/
+ sympcheck/
+