bin/build-binary-dist.sh: include the RGL in binary distributions

TODO: the corresponding changes in debian/rules
2018-11-28 17:27:29 +01:00
parent 8560b4fb65
commit 32ce03dc94
2 changed files with 18 additions and 1 deletions
--- a/WebSetup.hs
+++ b/WebSetup.hs
@@ -70,7 +70,7 @@ buildWeb gf flags (pkg,lbi) = do
        gf_lib_path = datadir (absoluteInstallDirs pkg lbi dest) </> "lib"
        args = numJobs flags++["-make","-s"] -- ,"-optimize-pgf"
               ++["--gfo-dir="++tmp_dir,
-                  "--gf-lib-path="++gf_lib_path,
+                --"--gf-lib-path="++gf_lib_path,
                  "--name="++dropExtension pgf,
                  "--output-dir="++gfo_dir]
               ++[dir</>file|file<-src]