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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
# Only GNU make should be used. The real makefile is GNUmakefile.
# The following include all targets in GNUmakefile, obtained by:
# grep '^[a-zA-Z].*:' GNUmakefile
all: err
small:
echo 'Target "small" is no longer supported. Use "make large" or simply "make".'
exit 1
acl2r: err
protections: err
chmod_image: err
do_saved: err
check_compile_ok: err
check_init_ok: err
fast: err
check: err
compile-ok: err
very-fast: err
fast-meter: err
check-sum: err
full: err
full-meter: err
copy: err
copy-distribution: err
copy-workshops: err
copy-nonstd: err
copy-developers: err
TAGS: err
move-to-old: err
move-new: err
init: err
proofs: err
DOC: err
TEXINFO: err
HTML: err
clean: err
red: err
large: err
large-acl2r: err
move-large: err
certify-books: err
regression: err
regression-nonstd: err
certify-books-fresh: err
regression-fresh: err
regression-nonstd-fresh: err
certify-books-short: err
certify-books-test: err
infix-init: err
infix-init10: err
infix-fin: err
clean-doc: err
clean-books: err
clean-books-nonstd: err
tar: err
tar-workshops: err
tar-nonstd: err
test: err
big-test: err
arch: err
mini-proveall: err
allegro-app: err
err:
@echo "ERROR:"
@echo "Apparently you are using other than GNU make"
@echo "(which MIGHT be found in /lusr/gnu/bin/make)."
@echo "Only GNU make is supported. If you think your"
@echo "'make' might work, you can move or delete"
@echo "ACL2's Makefile and copy or rename ACL2's"
@echo "GNUmakefile to Makefile."
@echo "Exiting with error...."
@exit 1
|
