diff options
Diffstat (limited to 'src/server')
| -rw-r--r-- | src/server/Setup.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/server/Setup.hs b/src/server/Setup.hs index 41a3edc7d..f0e23432c 100644 --- a/src/server/Setup.hs +++ b/src/server/Setup.hs @@ -29,7 +29,7 @@ example_grammars = ("Letter.pgf","letter", ".."</>".."</>"examples"</>"letter"</>"Letter???.gf")] -minibar_src = ".."</>"runtime"</>"javascript"</>"minibar" +minibar_src = ".."</>"www"</>"minibar" -------------------------------------------------------------------------------- instWWW args flags pki lbi = setupWWW args dest pki lbi |