check in documentation; update makefile and gitignore

sampsyo · Oct 10, 2023 · 801db70 · 801db70
1 parent 28e57b5
commit 801db70
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 1 deletion.
diff --git a/fastbril/Makefile b/fastbril/Makefile
@@ -4,6 +4,7 @@ BUILD_DIR ?= ./build
 SRC_DIRS ?= ./src
 CONGIG_DiR ?= ./config
 DOC_DIR ?= ./doc
+SHELL = /bin/sh
 
 CONFIGS := $(shell find ./config/ -name "*.cf")
 GEN_HEAD := $(shell for FILE in $(CONFIGS); do echo $$FILE | awk -F'[/.]' '{printf "src/%s.h\n", $$4}'; done)

diff --git a/fastbril/doc/.gitignore b/fastbril/doc/.gitignore
@@ -1,3 +1,8 @@
 *.aux
 *.out
-*.log
+*.log
+base.tex
+float.tex
+mem.tex
+ssa.tex
+types.tex
diff --git a/fastbril/doc/brb.pdf b/fastbril/doc/brb.pdf