]> https://gitweb.dealii.org/ - parameter_gui.git/commitdiff
projects / parameter_gui.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | combined (merge: 4444fdc ffca655)
Merge pull request #18 from gassmoeller/settings_ini_location
authorWolfgang Bangerth <bangerth@colostate.edu>
Sat, 24 Jun 2017 02:47:58 +0000 (21:47 -0500)
committerGitHub <noreply@github.com>
Sat, 24 Jun 2017 02:47:58 +0000 (21:47 -0500)
Use global settings instead of settings file for info message


Trivial merge
Mirror of the development repository for the Parameter Gui

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.