Commit graph

533 commits

Author SHA1 Message Date
92dc505b06
use caches to speed up compilation 2023-10-19 12:56:19 +02:00
9225c03547
remove unneded script 2023-10-19 10:55:10 +02:00
b1925a752f
fix TEXINPUTS 2023-10-19 10:42:01 +02:00
e7f4d10438
further try 2023-10-19 10:25:55 +02:00
6ae8238e15
next try 2023-10-19 10:08:20 +02:00
8bed099045
further attempt to compile correctly 2023-10-19 09:55:20 +02:00
13bbc42e4e
fix ci file 2023-10-19 02:56:31 +02:00
7be9e1046b
fix compilation 2023-10-19 02:55:29 +02:00
eaf0763583
correctly compile in pipeline 2023-10-19 02:50:36 +02:00
72cc9d78b0
set -e for compilation script 2023-10-19 02:49:26 +02:00
34f0a41699
change job name 2023-10-19 02:47:45 +02:00
c07e84d91b
generate documentation on master 2023-10-19 02:23:39 +02:00
8798571831
fix path 2023-10-19 02:21:55 +02:00
823c5097ce
adjust ci to new build style 2023-10-19 02:21:13 +02:00
6d8a131865
Rework building of documentation files
Instead of an ugly Makefile structure, we now use a single compile
script that collects all the files in build/doc.
2023-10-19 01:34:46 +02:00
b587beb806
use single job 2023-10-18 18:46:34 +02:00
ed6ee5ec64
remove unneeded ssh step 2023-10-18 16:35:40 +02:00
2cd113166d
update readme 2023-10-18 16:28:52 +02:00
6263366b56
adapt commit message in build repo 2023-10-18 16:25:41 +02:00
0156ddca43
fix origin url 2023-10-18 16:21:37 +02:00
476b57d2ba
fix permissions on ssh key 2023-10-18 16:03:51 +02:00
3858718041
change setting up git: don't use agent, directly write to ~/.ssh 2023-10-18 16:01:37 +02:00
e8fedd07a0
configure git directly before building 2023-10-18 15:51:43 +02:00
65c801c212
rename deploy key secret 2023-10-18 11:31:12 +02:00
f941a10fe6
correct domain for host key 2023-10-18 11:27:37 +02:00
5a0ec99d86
enter remote host key 2023-10-18 11:25:56 +02:00
3c8f825e3f
fix push 2023-10-18 11:24:21 +02:00
7e76546afd
fix pushing to build repo 2023-10-18 11:19:33 +02:00
d5af0e7ad1
fix ssh url 2023-10-18 11:16:37 +02:00
4719ba2d52
explicitly use ssh to clone 2023-10-18 11:15:23 +02:00
e0b9b7ad44
fix ref name 2023-10-18 11:13:58 +02:00
7c3775828e
clone history as well 2023-10-18 11:12:09 +02:00
546a7007cc
fetch tags 2023-10-18 11:11:01 +02:00
4008cb355f
clone submodules 2023-10-18 11:06:35 +02:00
298e515a51
fix environment variable 2023-10-18 11:04:38 +02:00
896956f6fa
fix ref name context variable 2023-10-18 10:26:11 +02:00
77140598bf
fix repo url 2023-10-18 10:21:00 +02:00
27a592b9f1
specify branch to checkout 2023-10-18 10:11:47 +02:00
1de88c00b8
rename deploy key variable 2023-10-18 09:56:35 +02:00
0aece45a9c
move ci file to corect location 2023-10-18 09:52:14 +02:00
6aa92357e0
ajust ci 2023-10-18 09:51:02 +02:00
3483a24dca
disable indexing with beamer clas 2023-06-18 21:15:50 +02:00
51afbd7188
add category of presheaves 2022-10-17 18:34:37 +02:00
521ce5c804
fix whitespace around \vocab 2022-08-18 16:09:02 +02:00
b6a13cfa40
add green background style 2022-08-18 11:32:37 +02:00
2d16a2d72a make todo commands accept optional arguments 2022-06-27 17:33:08 +02:00
8c5b9ad7a4 load missing decorations library for tikz-cd 2022-06-27 17:10:15 +02:00
e9f75cd220 fix error in category declaration 2022-06-27 16:46:26 +02:00
80377fc784 fix error in csv: use quotechar | correctly 2022-06-27 16:31:41 +02:00
aaa93783b2 fix error in csv dictionary: use proper quotechar | 2022-06-27 16:21:30 +02:00