update_library.anubis
1.07 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
read tools/basis.anubis
define String target_dir = "/home/alp/anubis_distrib/".
define String source_dir = "/home/alp/anubis_dev/".
define One
update_directory
(
String dir
).
define One
update_file
(
String dir,
FileDescription d
) =
if d is
{
no_info(_) then unique,
file(name,_,_,_) then print("Copying '"+dir+"/"+name+"'.\n");
forget(execute("cp",[source_dir+dir+"/"+name,target_dir+dir+"/"+name])),
link(_,_,_,_) then unique,
directory(name,_,_) then if name = "CVS"
then unique
else update_directory(dir+"/"+name)
}.
define One
update_directory
(
String dir
) =
with names = directory_full_list(target_dir+dir,"*","no_link","*"),
map_forget((FileDescription d) |-> update_file(dir,d),names).
global define One
update_library
(
List(String) args
) =
update_directory("library").