diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile index cdeaa65fbabc6fdcbcd072b58387dd47bd62029c..94d8f6148ccf99409a28556efa0b2e4dcda8024f 100644 --- a/doc/developer/tutorial/hello/Makefile +++ b/doc/developer/tutorial/hello/Makefile @@ -104,6 +104,7 @@ generated/makefile_multiple: generated/src/help_msg.ml \ generated/with_test: generated/src/run_call_print_bug.ml \ generated/src/tests/hello/hello_test.c \ + generated/src/tests/hello/oracle/hello_test.res.oracle \ generated/src/Makefile.test mkdir -p $@ cp generated/makefile_multiple/hello_options.ml $@/hello_options.ml @@ -112,8 +113,9 @@ generated/with_test: generated/src/run_call_print_bug.ml \ cp generated/src/run_call_print_bug.ml $@/hello_run_bug.ml echo "" >> $@/hello_run_bug.ml cat generated/src/extend_run.ml >> $@/hello_run_bug.ml - mkdir -p $@/tests/hello + mkdir -p $@/tests/hello/oracle cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c + cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle cp generated/src/Makefile.test $@/Makefile generated/with_doc: generated/src/help_msg.ml \ diff --git a/doc/developer/tutorial/hello/src/hello_test.c b/doc/developer/tutorial/hello/src/hello_test.c index 6ee10eeafa3bf084d6bb579ed00d4b31076b3a4b..9fcbfc12af7290704fe8367dfa4c18c556751347 100644 --- a/doc/developer/tutorial/hello/src/hello_test.c +++ b/doc/developer/tutorial/hello/src/hello_test.c @@ -1,3 +1,4 @@ /* run.config + PLUGIN: Hello OPT: -hello - */ \ No newline at end of file + */ diff --git a/doc/developer/tutorial/hello/src/hello_test.res.oracle b/doc/developer/tutorial/hello/src/hello_test.res.oracle index 32e9c05eee637f6c2347a8584c15369651faaa6a..5f6ab2389a8695bba00d6527d2135e7cc3389c6b 100644 --- a/doc/developer/tutorial/hello/src/hello_test.res.oracle +++ b/doc/developer/tutorial/hello/src/hello_test.res.oracle @@ -1,2 +1,2 @@ -[kernel] Parsing tests/hello/hello_test.c (with preprocessing) +[kernel] Parsing hello_test.c (with preprocessing) [hello] Hello, world!