Commit 0a7217247acafc8067765c872ae79e617a550aad

Thomas de Grivel 2023-09-29T18:10:23

readme: adding or removing files

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
diff --git a/README.md b/README.md
index ee3a03e..401ad6d 100644
--- a/README.md
+++ b/README.md
@@ -60,6 +60,15 @@ make gdb_ic3
 make gdb_test
 ```
 
+### Adding or removing files from the source tree
+```sh
+make gen
+./update_sources
+```
+
+Don't forget to commit your files and the modified sources.mk and
+sources.sh files.
+
 
 ## Structure