Browse Source

Move Ur/Web install script into framework directory

Adam Chlipala 11 years ago
parent
commit
d0506703db
2 changed files with 9 additions and 12 deletions
  1. 9 1
      frameworks/Ur/urweb/install.sh
  2. 0 11
      toolset/setup/linux/languages/urweb.sh

+ 9 - 1
frameworks/Ur/urweb/install.sh

@@ -1,3 +1,11 @@
 #!/bin/bash
 #!/bin/bash
 
 
-fw_depends urweb
+RETCODE=$(fw_exists /usr/local/bin/urweb)
+[ ! "$RETCODE" == 0 ] || { return 0; }
+
+fw_get http://www.impredicative.com/ur/urweb-20140819.tgz
+fw_untar urweb-20140819.tgz
+cd urweb-20140819
+./configure
+make
+sudo make install

+ 0 - 11
toolset/setup/linux/languages/urweb.sh

@@ -1,11 +0,0 @@
-#!/bin/bash
-
-RETCODE=$(fw_exists /usr/local/bin/urweb)
-[ ! "$RETCODE" == 0 ] || { return 0; }
-
-fw_get http://www.impredicative.com/ur/urweb-20140819.tgz
-fw_untar urweb-20140819.tgz
-cd urweb-20140819
-./configure
-make
-sudo make install