]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/README
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
[helm.git] / helm / metadata / README
1 To generate the metadata and refill the DB:
2
3 make indexes
4 make fill_db.sql
5 make drop_tables
6 make create_tables
7 make fill_db
8 cd dc
9 make drop_tables
10 make create_tables
11 make fill_db
Unnamed repository; edit this file 'description' to name the repository.